publication . Article . Preprint . 2015

Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses

Fabio Fioravanti; Emanuele De Angelis; Maurizio Proietti; Alberto Pettorossi;
Open Access
  • Published: 21 Jul 2015 Journal: Theory and Practice of Logic Programming, volume 15, pages 635-650 (issn: 1471-0684, eissn: 1475-3081, Copyright policy)
  • Publisher: Cambridge University Press (CUP)
Abstract
We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form $\{\varphi\}$ prog $\{\psi\}$, where the assertions $\varphi$ and $\psi$ are predicates defined by a set Spec of possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also called constrained Horn clauses). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that $\{\varphi\}$ prog $\{\psi\}$ is valid. We highlight some limitations of state-of...
Read more
doi: 10.1017/s1471068415000289
Subjects
arXiv: Computer Science::Logic in Computer ScienceComputer Science::Programming Languages
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Theoretical Computer Science, Hardware and Architecture, Computational Theory and Mathematics, Software, Artificial Intelligence, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Unit propagation, Correctness, Discrete mathematics, Program transformation, Computer science, Satisfiability, Horn-satisfiability, Horn clause, Algorithm, Linearization, Constraint logic programming
Download fromView all 2 versions
Theory and Practice of Logic Programming
Article
Provider: UnpayWall
arXiv.org e-Print Archive
Preprint . 2015
Provider: arXiv.org e-Print Archive
Theory and Practice of Logic Programming
Article
Provider: Microsoft Academic Graph
Theory and Practice of Logic Programming
Article . 2015
Provider: Crossref
37 references, page 1 of 3

Albert, E., Go´mez-Zamalloa, M., Hubert, L., and Puebla, G. 2007. Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In Practical Aspects of Declarative Languages, M. Hanus, Ed. Lecture Notes in Computer Science 4354. Springer, 124-139.

Apt, K. R., de Boer, F. S., and Olderog, E.-R. 2009. Verification of Sequential and Concurrent Programs, Third ed. Springer. [OpenAIRE]

Benoy, F. and King, A. 1997. Inferring argument size relationships with CLP(R). In Proceedings of the 6th International Workshop on Logic Program Synthesis and Transformation, LOPSTR '96, Stockholm, Sweden, August 28-30, 1996, J. P. Gallagher, Ed. Lecture Notes in Computer Science 1207. Springer, 204-223.

Bjørner, N., McMillan, K., and Rybalchenko, A. 2012. Program verification as satisfiability modulo theories. In Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, SMT-COMP '12. 3-11.

Cimatti, A., Griggio, A., Schaafsma, B., and Sebastiani, R. 2013. The MathSAT5 SMT Solver. In Proceedings of TACAS, N. Piterman and S. Smolka, Eds. Lecture Notes in Computer Science 7795. Springer. [OpenAIRE]

Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proceedings of the 4th ACM-SIGPLAN Symposium on Principles of Programming Languages, POPL '77. ACM, 238-252.

Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, POPL '78. ACM, 84-96. [OpenAIRE]

De Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M. 2014a. Program verification via iterated specialization. Science of Computer Programming 95, Part 2, 149-175. Selected and extended papers from Partial Evaluation and Program Manipulation 2013. [OpenAIRE]

De Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M. 2014b. VeriMAP: A Tool for Verifying Programs through Transformations. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '14. Lecture Notes in Computer Science 8413. Springer, 568-574. Available at: http://www.map.uniroma2.it/VeriMAP.

de Moura, L. M. and Bjørner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08. Lecture Notes in Computer Science 4963. Springer, 337-340.

De Schreye, D., Glu¨ck, R., Jørgensen, J., Leuschel, M., Martens, B., and Sørensen, M. H. 1999. Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments. Journal of Logic Programming 41, 2-3, 231-277.

Etalle, S. and Gabbrielli, M. 1996. Transformations of CLP modules. Theoretical Computer Science 166, 101-146. [OpenAIRE]

Felsing, D., Grebing, S., Klebanov, V., Ru¨mmer, P., and Ulbrich, M. 2014. Automating Regression Verification. In Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE '14. ACM, 349-360. [OpenAIRE]

Fioravanti, F., Pettorossi, A., Proietti, M., and Senni, V. 2013. Generalization strategies for the verification of infinite state systems. Theory and Practice of Logic Programming. Special Issue on the 25th Annual GULP Conference 13, 2, 175-199.

Grebenshchikov, S., Lopes, N. P., Popeea, C., and Rybalchenko, A. 2012. Synthesizing software verifiers from proof rules. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12. 405-416. [OpenAIRE]

37 references, page 1 of 3
Related research
Abstract
We present a method for verifying the correctness of imperative programs which is based on the automated transformation of their specifications. Given a program prog, we consider a partial correctness specification of the form $\{\varphi\}$ prog $\{\psi\}$, where the assertions $\varphi$ and $\psi$ are predicates defined by a set Spec of possibly recursive Horn clauses with linear arithmetic (LA) constraints in their premise (also called constrained Horn clauses). The verification method consists in constructing a set PC of constrained Horn clauses whose satisfiability implies that $\{\varphi\}$ prog $\{\psi\}$ is valid. We highlight some limitations of state-of...
Read more
doi: 10.1017/s1471068415000289
Subjects
arXiv: Computer Science::Logic in Computer ScienceComputer Science::Programming Languages
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Theoretical Computer Science, Hardware and Architecture, Computational Theory and Mathematics, Software, Artificial Intelligence, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Unit propagation, Correctness, Discrete mathematics, Program transformation, Computer science, Satisfiability, Horn-satisfiability, Horn clause, Algorithm, Linearization, Constraint logic programming
Download fromView all 2 versions
Theory and Practice of Logic Programming
Article
Provider: UnpayWall
arXiv.org e-Print Archive
Preprint . 2015
Provider: arXiv.org e-Print Archive
Theory and Practice of Logic Programming
Article
Provider: Microsoft Academic Graph
Theory and Practice of Logic Programming
Article . 2015
Provider: Crossref
37 references, page 1 of 3

Albert, E., Go´mez-Zamalloa, M., Hubert, L., and Puebla, G. 2007. Verification of Java Bytecode Using Analysis and Transformation of Logic Programs. In Practical Aspects of Declarative Languages, M. Hanus, Ed. Lecture Notes in Computer Science 4354. Springer, 124-139.

Apt, K. R., de Boer, F. S., and Olderog, E.-R. 2009. Verification of Sequential and Concurrent Programs, Third ed. Springer. [OpenAIRE]

Benoy, F. and King, A. 1997. Inferring argument size relationships with CLP(R). In Proceedings of the 6th International Workshop on Logic Program Synthesis and Transformation, LOPSTR '96, Stockholm, Sweden, August 28-30, 1996, J. P. Gallagher, Ed. Lecture Notes in Computer Science 1207. Springer, 204-223.

Bjørner, N., McMillan, K., and Rybalchenko, A. 2012. Program verification as satisfiability modulo theories. In Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, SMT-COMP '12. 3-11.

Cimatti, A., Griggio, A., Schaafsma, B., and Sebastiani, R. 2013. The MathSAT5 SMT Solver. In Proceedings of TACAS, N. Piterman and S. Smolka, Eds. Lecture Notes in Computer Science 7795. Springer. [OpenAIRE]

Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proceedings of the 4th ACM-SIGPLAN Symposium on Principles of Programming Languages, POPL '77. ACM, 238-252.

Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, POPL '78. ACM, 84-96. [OpenAIRE]

De Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M. 2014a. Program verification via iterated specialization. Science of Computer Programming 95, Part 2, 149-175. Selected and extended papers from Partial Evaluation and Program Manipulation 2013. [OpenAIRE]

De Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M. 2014b. VeriMAP: A Tool for Verifying Programs through Transformations. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '14. Lecture Notes in Computer Science 8413. Springer, 568-574. Available at: http://www.map.uniroma2.it/VeriMAP.

de Moura, L. M. and Bjørner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08. Lecture Notes in Computer Science 4963. Springer, 337-340.

De Schreye, D., Glu¨ck, R., Jørgensen, J., Leuschel, M., Martens, B., and Sørensen, M. H. 1999. Conjunctive Partial Deduction: Foundations, Control, Algorithms, and Experiments. Journal of Logic Programming 41, 2-3, 231-277.

Etalle, S. and Gabbrielli, M. 1996. Transformations of CLP modules. Theoretical Computer Science 166, 101-146. [OpenAIRE]

Felsing, D., Grebing, S., Klebanov, V., Ru¨mmer, P., and Ulbrich, M. 2014. Automating Regression Verification. In Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE '14. ACM, 349-360. [OpenAIRE]

Fioravanti, F., Pettorossi, A., Proietti, M., and Senni, V. 2013. Generalization strategies for the verification of infinite state systems. Theory and Practice of Logic Programming. Special Issue on the 25th Annual GULP Conference 13, 2, 175-199.

Grebenshchikov, S., Lopes, N. P., Popeea, C., and Rybalchenko, A. 2012. Synthesizing software verifiers from proof rules. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12. 405-416. [OpenAIRE]

37 references, page 1 of 3
Related research
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue