# Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses

- 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)

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]

###### Related research

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]