{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:20:22Z","timestamp":1784233222033,"version":"3.55.0"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2017,12,4]],"date-time":"2017-12-04T00:00:00Z","timestamp":1512345600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2018,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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<jats:italic>predicate abstraction<\/jats:italic>are sometimes unable to verify satisfiability because they look for models that are definable in a given class \ud835\udcd0 of constraints, called \ud835\udcd0-definable models. We introduce a transformation technique, called<jats:italic>Predicate Pairing<\/jats:italic>, 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 \ud835\udcd0-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 \ud835\udcd0, the unfold\/fold transformation rules preserve the existence of an \ud835\udcd0-definable model, that is, if the original clauses have an \ud835\udcd0-definable model, then the transformed clauses have an \ud835\udcd0-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an \ud835\udcd0-definable model<jats:italic>if and only if<\/jats:italic>the original ones have an \ud835\udcd0-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 \ud835\udcd0-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 \ud835\udcd0-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<jats:italic>relational properties of programs<\/jats:italic>, 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.<\/jats:p>","DOI":"10.1017\/s1471068417000497","type":"journal-article","created":{"date-parts":[[2017,12,4]],"date-time":"2017-12-04T07:37:02Z","timestamp":1512373022000},"page":"126-166","source":"Crossref","is-referenced-by-count":12,"title":["Predicate Pairing for program verification"],"prefix":"10.1017","volume":"18","author":[{"given":"EMANUELE","family":"DE ANGELIS","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"FABIO","family":"FIORAVANTI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7858-4032","authenticated-orcid":false,"given":"ALBERTO","family":"PETTOROSSI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3835-4931","authenticated-orcid":false,"given":"MAURIZIO","family":"PROIETTI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2017,12,4]]},"reference":[{"key":"S1471068417000497_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S147106840200145X"},{"key":"S1471068417000497_ref34","doi-asserted-by":"crossref","unstructured":"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, B. Meyer , L. Baresi , and M. Mezini , Eds., ACM, 345\u2013355.","DOI":"10.1145\/2491411.2491452"},{"key":"S1471068417000497_ref31","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.scico.2017.01.002","article-title":"Constraint specialisation in Horn clause verification","volume":"137","author":"Kafle","year":"2017","journal-title":"Science of Computer Programming"},{"key":"#cr-split#-S1471068417000497_ref3.1","doi-asserted-by":"crossref","unstructured":"2. Benoy F. and King A. 1997. Inferring argument size relationships with CLP","DOI":"10.1007\/3-540-62718-9_12"},{"key":"#cr-split#-S1471068417000497_ref3.2","unstructured":"3. (R). In Proc. 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, Vol. 1207. Springer, 204-223."},{"key":"S1471068417000497_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"S1471068417000497_ref28","unstructured":"Hojjat H. , Konecn\u00fd F. , Garnier F. , Iosif R. , Kuncak V. and R\u00fcmmer 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, D. Giannakopoulou and D. M\u00e9ry , Eds., Lecture Notes in Computer Science, Vol. 7436. Springer, 247\u2013251."},{"key":"S1471068417000497_ref45","doi-asserted-by":"crossref","unstructured":"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, M. Hanus , Ed., Lecture Notes in Computer Science, Vol. 4354. Springer, 245\u2013259.","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"S1471068417000497_ref27","unstructured":"Hoder K. , Bj\u00f8rner N. and de Moura L. M. 2011. \u03bc Z\u2013 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, G. Gopalakrishnan and S. Qadeer , Eds., Lecture Notes in Computer Science, Vol. 6806. Springer, 457\u2013462."},{"key":"S1471068417000497_ref30","first-page":"454","volume-title":"Principles and Practice of Constraint Programming, CP '09","author":"Jaffar","year":"2009"},{"key":"S1471068417000497_ref25","doi-asserted-by":"crossref","unstructured":"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\u2013361.","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"S1471068417000497_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8"},{"key":"S1471068417000497_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"#cr-split#-S1471068417000497_ref41.1","unstructured":"8. M??ndez-Lojo M., Navas J. A. and Hermenegildo M. V. 2008. A flexible,"},{"key":"#cr-split#-S1471068417000497_ref41.2","doi-asserted-by":"crossref","unstructured":"9. (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.","DOI":"10.1007\/978-3-540-78769-3_11"},{"key":"S1471068417000497_ref9","doi-asserted-by":"crossref","unstructured":"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\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"S1471068417000497_ref8","unstructured":"Ciob\u00e2c\u0103 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 \u2013 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014, S. Merz and J. Pang , Eds., Lecture Notes in Computer Science, Vol. 8829. Springer, 75\u201390."},{"key":"S1471068417000497_ref10","unstructured":"De Angelis E. , Fioravanti F. , Pettorossi A. and Proietti M. 2014a. Program verification via iterated specialization. Science of Computer Programming 95, Part 2, 149\u2013175. Selected and extended papers from Partial Evaluation and Program Manipulation 2013."},{"key":"S1471068417000497_ref6","unstructured":"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\u2013442."},{"key":"S1471068417000497_ref2","doi-asserted-by":"crossref","unstructured":"Barthe G. , Crespo J. M. and Kunz C. 2011. Relational verification using product programs. In Proc. of FM 2011: Formal Methods \u2013 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Lecture Notes in Computer Science, Vol. 6664. Springer, 200\u2013214.","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"S1471068417000497_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90028-0"},{"key":"S1471068417000497_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"S1471068417000497_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-008-0075-2"},{"key":"S1471068417000497_ref13","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2015-1257"},{"key":"S1471068417000497_ref1","unstructured":"Albert E. , G\u00f3mez-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, M. Hanus , Ed., Lecture Notes in Computer Science, Vol. 4354. Springer, 124\u2013139."},{"key":"S1471068417000497_ref7","doi-asserted-by":"crossref","unstructured":"Chaki S. , Gurfinkel A. and Strichman O. 2012. Regression verification for multi-threaded programs. In Proc. of Verification, Model Checking, and Abstract Interpretation \u2013 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012, V. Kuncak and A. Rybalchenko , Eds., Lecture Notes in Computer Science, Vol. 7148. Springer, 119\u2013135.","DOI":"10.1007\/978-3-642-27940-9_9"},{"key":"S1471068417000497_ref4","doi-asserted-by":"crossref","unstructured":"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\u201325.","DOI":"10.1145\/964001.964003"},{"key":"S1471068417000497_ref15","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1016\/j.scico.2016.11.002","article-title":"Semantics-based generation of verification conditions via program specialization","volume":"147","author":"De","year":"2017","journal-title":"Science of Computer Programming"},{"key":"S1471068417000497_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90050-7"},{"key":"S1471068417000497_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000289"},{"key":"S1471068417000497_ref46","unstructured":"R\u00fcmmer 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, N. Sharygina and H. Veith , Eds., Lecture Notes in Computer Science, Vol. 8044. Springer, 347\u2013363."},{"key":"S1471068417000497_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"S1471068417000497_ref32","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/j.cl.2015.11.001","article-title":"Horn clause verification with convex polyhedral abstraction and tree automata-based refinement","volume":"47","author":"Kafle","year":"2017","journal-title":"Computer Languages, Systems and Structures"},{"key":"S1471068417000497_ref14","doi-asserted-by":"crossref","unstructured":"De 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, X. Rival , Ed., Lecture Notes in Computer Science, Vol. 9837. Springer, 147\u2013169.","DOI":"10.1007\/978-3-662-53413-7_8"},{"key":"S1471068417000497_ref40","volume-title":"Introduction to Mathematical Logic","author":"Mendelson","year":"1997"},{"key":"S1471068417000497_ref16","unstructured":"de Moura, L. M. and Bj\u00f8rner 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\u2013340."},{"key":"S1471068417000497_ref21","doi-asserted-by":"crossref","unstructured":"Felsing D. , Grebing S. , Klebanov V. , R\u00fcmmer 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, I. Crnkovic , M. Chechik , and P. Gr\u00fcnbacher , Eds., 349\u2013360.","DOI":"10.1145\/2642937.2642987"},{"key":"S1471068417000497_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S1471068417000497_ref33","doi-asserted-by":"crossref","unstructured":"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 \u2013 28th International Conference, CAV 2016, Part I Toronto, ON, Canada, July 17-23, 2016. Lecture Notes in Computer Science, Vol. 9779. Springer, 261\u2013268.","DOI":"10.1007\/978-3-319-41528-4_14"},{"key":"S1471068417000497_ref17","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/S0743-1066(99)00030-8","article-title":"Conjunctive partial deduction: Foundations, control, algorithms, and experiments","volume":"41","author":"De","year":"1999","journal-title":"Journal of Logic Programming"},{"key":"S1471068417000497_ref5","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II \u2013 Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday","author":"Bj\u00f8rner","year":"2015"},{"key":"S1471068417000497_ref39","unstructured":"McMillan K. L. and Rybalchenko A. 2013. Solving constrained Horn clauses using interpolation. MSR Technical Report 2013-6, Microsoft Report."},{"key":"S1471068417000497_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00148-4"},{"key":"S1471068417000497_ref20","doi-asserted-by":"crossref","unstructured":"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, S. Chaudhuri and A. Farzan , Eds., Lecture Notes in Computer Science, Vol. 7792. Springer International Publishing.","DOI":"10.1007\/978-3-319-41540-6_24"},{"key":"S1471068417000497_ref22","unstructured":"Ganty P. , Iosif R. and Kone\u010dn\u00fd 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, N. Piterman , Scott A. Smolka , Eds., Lecture Notes in Computer Science, Vol. 7795. Springer, 245\u2013259."},{"key":"S1471068417000497_ref48","unstructured":"Tamaki H. and Sato T. 1984. Unfold\/fold transformation of logic programs. In Proc. of the Second International Conference on Logic Programming, ICLP '84, S.-\u00c5. T\u00e4rnlund , Ed., Uppsala University, Uppsala, Sweden, 127\u2013138."},{"key":"S1471068417000497_ref50","doi-asserted-by":"crossref","unstructured":"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. J. Cu\u00e9llar , T. S. E. Maibaum , and K. Sere , Eds., Lecture Notes in Computer Science, Vol. 5014. Springer, 35\u201351.","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"S1471068417000497_ref38","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/s10009-015-0366-1","article-title":"Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic","volume":"18","author":"Lopes","year":"2016","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"S1471068417000497_ref47","doi-asserted-by":"crossref","unstructured":"Strichman O. and Veitsman M. 2016. Regression verification for unbalanced recursive functions. In Proc. of FM 2016: Formal Methods \u2013 21st International Symposium, Limassol, Cyprus, November 9-11, 2016. Lecture Notes in Computer Science, Vol. 9995. Springer International Publishing, 645\u2013658.","DOI":"10.1007\/978-3-319-48989-6_39"},{"key":"S1471068417000497_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362390"},{"key":"S1471068417000497_ref43","doi-asserted-by":"crossref","unstructured":"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, G. Levi , Ed., Lecture Notes in Computer Science, Vol. 1503. Springer, 246\u2013261.","DOI":"10.1007\/3-540-49727-7_15"},{"key":"S1471068417000497_ref11","doi-asserted-by":"crossref","unstructured":"De 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\u2013574. Available at: http:\/\/www.map.uniroma2.it\/VeriMAP.","DOI":"10.1007\/978-3-642-54862-8_47"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068417000497","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,9]],"date-time":"2022-08-09T21:19:46Z","timestamp":1660079986000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068417000497\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,4]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["S1471068417000497"],"URL":"https:\/\/doi.org\/10.1017\/s1471068417000497","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,4]]}}}