Hostname: page-component-cd9895bd7-jn8rn Total loading time: 0 Render date: 2024-12-25T05:37:51.088Z Has data issue: false hasContentIssue false
  • English
  • Français

Predicate Pairing for program verification

Published online by Cambridge University Press:  04 December 2017

EMANUELE DE ANGELIS ,
FABIO FIORAVANTI ,
ALBERTO PETTOROSSI Open the ORCID record for ALBERTO PETTOROSSI [Opens in a new window]  and
MAURIZIO PROIETTI Open the ORCID record for MAURIZIO PROIETTI [Opens in a new window]
EMANUELE DE ANGELIS
Affiliation:
DEC, ‘G. d'Annunzio’ University of Chieti-Pescara, Pescara, Italy (e-mails: [email protected], [email protected])
FABIO FIORAVANTI
Affiliation:
DEC, ‘G. d'Annunzio’ University of Chieti-Pescara, Pescara, Italy (e-mails: [email protected], [email protected])
ALBERTO PETTOROSSI
Affiliation:
DICII, University of Rome Tor Vergata, Rome, Italy (e-mails: [email protected])
MAURIZIO PROIETTI
Affiliation:
CNR-IASI, Rome, Italy (e-mails: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

It is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for constrained Horn clauses (or CHC solvers) based on predicate abstraction are sometimes unable to verify satisfiability because they look for models that are definable in a given class 𝓐 of constraints, called 𝓐-definable models. We introduce a transformation technique, called Predicate Pairing, which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an 𝓐-definable model, and hence can be effectively verified by a state-of-the-art CHC solver. In particular, we prove that, under very general conditions on 𝓐, the unfold/fold transformation rules preserve the existence of an 𝓐-definable model, that is, if the original clauses have an 𝓐-definable model, then the transformed clauses have an 𝓐-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an 𝓐-definable model if and only if the original ones have an 𝓐-definable model. Then, we present a strategy, called Predicate Pairing, which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability problem can be solved by looking for 𝓐-definable models. The Predicate Pairing (PP) strategy introduces a new predicate defined by the conjunction of two predicates occurring in the original set of clauses, together with a conjunction of constraints. We will show through some examples that an 𝓐-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We will also present some case studies showing that Predicate Pairing plays a crucial role in the verification of relational properties of programs, that is, properties relating two programs (such as program equivalence) or two executions of the same program (such as non-interference). Finally, we perform an experimental evaluation of the proposed techniques to assess the effectiveness of Predicate Pairing in increasing the power of CHC solving.

Keywords

program verificationconstrained Horn clausesconstraint logic programmingprogram transformationrelational properties of programs
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 18 , Special Issue 2: Computational Logic for Verification , March 2018 , pp. 126 - 166
Copyright
Copyright © Cambridge University Press 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Albert, E., Gómez-Zamalloa, M., Hubert, L. and Puebla, G. 2007. Verification of Java bytecode using analysis and transformation of logic programs. In Proc. of Practical Aspects of Declarative Languages, Hanus, M., Ed., Lecture Notes in Computer Science, Vol. 4354. Springer, 124–139.Google Scholar
Barthe, G., Crespo, J. M. and Kunz, C. 2011. Relational verification using product programs. In Proc. of FM 2011: Formal Methods – 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Lecture Notes in Computer Science, Vol. 6664. Springer, 200–214.Google Scholar
Benoy, F. and King, A. 1997. Inferring argument size relationships with CLP(R). In Proc. of the 6th International Workshop on Logic Program Synthesis and Transformation, LOPSTR'96, Stockholm, Sweden, August 28-30, 1996, Gallagher, J. P., Ed., Lecture Notes in Computer Science, Vol. 1207. Springer, 204–223.Google Scholar
Benton, N. 2004. Simple relational correctness proofs for static analyses and program transformations. In Proc. of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004. ACM, 14–25.Google Scholar
Bjørner, N., Gurfinkel, A., McMillan, K. L. and Rybalchenko, A. 2015. Horn clause solvers for program verification. In Fields of Logic and Computation II – Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Beklemishev, L. D., Blass, A., Dershowitz, N., Finkbeiner, B., and Schulte, W., Eds., Lecture Notes in Computer Science, Vol. 9300. Springer, Switzerland, 24–51.Google Scholar
Bradley, A. R., Manna, Z. and Sipma, H. B. 2006. What's decidable about arrays? In Proc. of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation. VMCAI '06. Lecture Notes in Computer Science, Vol. 3855. Springer, 427–442.Google Scholar
Chaki, S., Gurfinkel, A. and Strichman, O. 2012. Regression verification for multi-threaded programs. In Proc. of Verification, Model Checking, and Abstract Interpretation – 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, Kuncak, V. and Rybalchenko, A., Eds., Lecture Notes in Computer Science, Vol. 7148. Springer, 119–135.Google Scholar
Ciobâcă, S., Lucanu, D., Rusu, V. and Rosu, G. 2014. A language-independent proof system for mutual program equivalence. In Proc. of Formal Methods and Software Engineering – 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014, Merz, S. and Pang, J., Eds., Lecture Notes in Computer Science, Vol. 8829. Springer, 75–90.Google Scholar
Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proc. of the 4th ACM-SIGPLAN Symposium on Principles of Programming Languages, POPL '77. ACM, 238–252.Google Scholar
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.Google Scholar
DeAngelis, E. Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M. 2014b. VeriMAP: A tool for verifying programs through transformations. In Proc. of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '14. Lecture Notes in Computer Science, Vol. 8413. Springer, 568–574. Available at: http://www.map.uniroma2.it/VeriMAP.CrossRefGoogle Scholar
De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M. 2015a. Proving correctness of imperative programs by linearizing constrained Horn clauses. Theory and Practice of Logic Programming 15, 4–5, 635–650.Google Scholar
De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M. 2015b. A rule-based verification strategy for array manipulating programs. Fundamenta Informaticae 140, 3–4, 329–355.Google Scholar
DeAngelis, E. Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M. 2016. Relational verification through Horn clause transformation. In Proc. of the 23rd International Symposium on Static Analysis, SAS 2016, Edinburgh, UK, September 8-10, 2016, Rival, X., Ed., Lecture Notes in Computer Science, Vol. 9837. Springer, 147–169.Google Scholar
DeAngelis, E. Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M. 2017. Semantics-based generation of verification conditions via program specialization. Science of Computer Programming 147, 3–4, 78–108.Google Scholar
deMoura, L. M. Moura, L. M. and Bjørner, N. 2008. Z3: An efficient SMT solver. In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS '08. Lecture Notes in Computer Science, Vol. 4963. Springer, 337–340.Google Scholar
DeSchreye, D. Schreye, D., Glü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.Google Scholar
Debray, S. K. and Ramakrishnan, R. 1994. Abstract interpretation of logic programs using magic transformations. Journal of Logic Programming 18, 149–176.CrossRefGoogle Scholar
Etalle, S. and Gabbrielli, M. 1996. Transformations of CLP modules. Theoretical Computer Science 166, 101–146.Google Scholar
Fedyukovich, G., Gurfinkel, A. and Sharygina, N. 2016. Property directed equivalence via abstract simulation. In Proc. of Computer Aided Verification: 28th International Conference, CAV 2016, Part II, Toronto, Canada, July 17-23, 2016, Chaudhuri, S. and Farzan, A., Eds., Lecture Notes in Computer Science, Vol. 7792. Springer International Publishing.Google Scholar
Felsing, D., Grebing, S., Klebanov, V., Rümmer, P. and Ulbrich, M. 2014. Automating regression verification. In Proc. of ACM/IEEE International Conference on Automated Software Engineering, ASE '14, Vasteras, Sweden - September 15-19, 2014, Crnkovic, I., Chechik, M., and Grünbacher, P., Eds., 349–360.Google Scholar
Ganty, P., Iosif, R. and Konečný, F. 2013. Underapproximation of procedure summaries for integer programs. In Proc. of Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Piterman, N., Smolka, Scott A., Eds., Lecture Notes in Computer Science, Vol. 7795. Springer, 245–259.Google Scholar
Godlin, B. and Strichman, O. 2008. Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45, 6, 403–439.CrossRefGoogle Scholar
Grebenshchikov, S., Lopes, N. P., Popeea, C. and Rybalchenko, A. 2012. Synthesizing software verifiers from proof rules. In Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12. 405–416.CrossRefGoogle Scholar
Gurfinkel, A., Kahsai, T., Komuravelli, A. and Navas, J. 2015. The SeaHorn verification framework. In Proc. of Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015. Lecture Notes in Computer Science 9206. Springer, 343–361.Google Scholar
Hoare, C. 1969. An axiomatic basis for computer programming. Communications of the ACM 12, 10 (October), 576–580.Google Scholar
Hoder, K., Bjørner, N. and de Moura, L. M. 2011. μ Z– An efficient engine for fixed points with constraints. In Proc. of Computer Aided Verification, 23rd International Conference, CAV '11, Snowbird, UT, USA, July 14-20, 2011, Gopalakrishnan, G. and Qadeer, S., Eds., Lecture Notes in Computer Science, Vol. 6806. Springer, 457–462.Google Scholar
Hojjat, H., Konecný, F., Garnier, F., Iosif, R., Kuncak, V. and Rümmer, P. 2012. A verification toolkit for numerical transition systems. In Proc. of FM '12: Formal Methods, 18th International Symposium, Paris, France, August 27-31, 2012, Giannakopoulou, D. and Méry, D., Eds., Lecture Notes in Computer Science, Vol. 7436. Springer, 247–251.Google Scholar
Jaffar, J. and Maher, M. 1994. Constraint logic programming: A survey. Journal of Logic Programming 19/20, 503–581.CrossRefGoogle Scholar
Jaffar, J., Santosa, A. and Voicu, R. 2009. An interpolation method for CLP traversal. In Principles and Practice of Constraint Programming, CP '09, Gent, I., Ed., Lecture Notes in Computer Science, Vol. 5732. Springer, 454–469.Google Scholar
Kafle, B. and Gallagher, J. P. 2017a. Constraint specialisation in Horn clause verification. Science of Computer Programming 137, 125–140.Google Scholar
Kafle, B. and Gallagher, J. P. 2017b. Horn clause verification with convex polyhedral abstraction and tree automata-based refinement. Computer Languages, Systems & Structures 47, 2–18.CrossRefGoogle Scholar
Kafle, B., Gallagher, J. P., and Morales, J. F. 2016. RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata. In Proc. of Computer Aided Verification – 28th International Conference, CAV 2016, Part I Toronto, ON, Canada, July 17-23, 2016. Lecture Notes in Computer Science, Vol. 9779. Springer, 261–268.Google Scholar
Lahiri, S. K., McMillan, K. L., Sharma, R. and Hawblitzel, C. 2013. Differential assertion checking. In Proc. of Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, Saint Petersburg, Russian Federation, August 18-26, 2013, Meyer, B., Baresi, L., and Mezini, M., Eds., ACM, 345–355.Google Scholar
Leroy, X. 2009. Formal verification of a realistic compiler. Communications of the ACM 52, 7, 107–115.Google Scholar
Leuschel, M. and Bruynooghe, M. 2002. Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2, 4&5, 461–515.Google Scholar
Lloyd, J. W. 1987. Foundations of Logic Programming. Springer-Verlag, Berlin. 2nd Edition.Google Scholar
Lopes, N. P. and Monteiro, J. 2016. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. International Journal on Software Tools for Technology Transfer 18, 4, 359–374.Google Scholar
McMillan, K. L. and Rybalchenko, A. 2013. Solving constrained Horn clauses using interpolation. MSR Technical Report 2013-6, Microsoft Report.Google Scholar
Mendelson, E. 1997. Introduction to Mathematical Logic. Chapman & Hall, London, UK. 4th Edition.Google Scholar
Méndez-Lojo, M., Navas, J. A. and Hermenegildo, M. V. 2008. A flexible, (C)LP-based approach to the analysis of object-oriented programs. In Proc. of 17th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR '07, Kongens Lyngby, Denmark, August 23-24, 2007. Lecture Notes in Computer Science, Vol. 4915. Springer, 154–168.Google Scholar
Miné, A. 2006. The octagon abstract domain. Higher-Order and Symbolic Computation 19, 1, 31–100.Google Scholar
Peralta, J. C., Gallagher, J. P. and Saglam, H. 1998. Analysis of imperative programs through analysis of constraint logic programs. In Proc. of the 5th International Symposium on Static Analysis, SAS '98, Levi, G., Ed., Lecture Notes in Computer Science, Vol. 1503. Springer, 246–261.Google Scholar
Pettorossi, A. and Proietti, M. 1994. Transformation of logic programs: Foundations and techniques. Journal of Logic Programming 19,20, 261–320.CrossRefGoogle Scholar
Podelski, A. and Rybalchenko, A. 2007. ARMC: The logical choice for software model checking with abstraction refinement. In Proc. of Practical Aspects of Declarative Languages, PADL '07, Hanus, M., Ed., Lecture Notes in Computer Science, Vol. 4354. Springer, 245–259.Google Scholar
Rümmer, P., Hojjat, H. and Kuncak, V. 2013. Disjunctive interpolants for Horn clause verification. In Proc. of the 25th International Conference on Computer Aided Verification, CAV '13, Saint Petersburg, Russia, July 13-19, 2013, Sharygina, N. and Veith, H., Eds., Lecture Notes in Computer Science, Vol. 8044. Springer, 347–363.Google Scholar
Strichman, O. and Veitsman, M. 2016. Regression verification for unbalanced recursive functions. In Proc. of FM 2016: Formal Methods – 21st International Symposium, Limassol, Cyprus, November 9-11, 2016. Lecture Notes in Computer Science, Vol. 9995. Springer International Publishing, 645–658.Google Scholar
Tamaki, H. and Sato, T. 1984. Unfold/fold transformation of logic programs. In Proc. of the Second International Conference on Logic Programming, ICLP '84, Tärnlund, S.-Å., Ed., Uppsala University, Uppsala, Sweden, 127–138.Google Scholar
Verdoolaege, S., Janssens, G. and Bruynooghe, M. 2012. Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34, 3, 11.Google Scholar
Zaks, A. and Pnueli, A. 2008. CoVaC: Compiler validation by program analysis of the cross-product. In Proc. of the 15th International Symposium on Formal Methods (FM 2008), Turku, Finland, May 26-30, 2008. Cuéllar, J., Maibaum, T. S. E., and Sere, K., Eds., Lecture Notes in Computer Science, Vol. 5014. Springer, 35–51.Google Scholar