Abstract
One of the main challenges in software verification is efficient and precise analysis of programs with procedures and loops. Interpolation methods remain among the most promising techniques for such verification. To accommodate the demands of various programming language features, over the past years several extended forms of interpolation have been introduced. We give a precise ontology of such extended interpolation methods, and investigate the relationship between interpolation and fragments of constrained recursion-free Horn clauses. We also introduce a new notion of interpolation, disjunctive interpolation, which solves a more general class of problems in one step compared to previous notions of interpolants, such as tree interpolants or inductive sequences of interpolants. We present algorithms and complexity for construction of interpolants, as well as the corresponding decision problems for recursion-free Horn fragments. Finally, we give an extensive empirical evaluation using a solver for (recursive) Horn problems, in particular comparing the performance of tree interpolation and disjunctive interpolation for constraints modelling software verification tasks.
Similar content being viewed by others
Notes
http://z3.codeplex.com, version 4.3.2.
References
Albarghouthi A, Gurfinkel A, Chechik M (2012) Craig interpretation. In: SAS
Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI, pp 39–55
Ball T, Podelski, A, Rajamani SK (2002) Relative completeness of abstraction refinement for software model checking. In: TACAS’02, LNCS, vol 2280, p 158
Banda G, Gallagher JP (2009) Analysis of linear hybrid systems in clp. In: Hanus [20], pp 55–70. doi:10.1007/978-3-642-00515-2_5
Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified Horn clauses. In: CAV
Beyer D (2014) Status report on software verification—(competition summary sv-comp 2014). In: TACAS, pp 373–388
Bjørner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified Horn clauses. In: SAS
Brillout A, Kroening D, Rümmer P, Wahl T (2011) An interpolating sequent calculus for quantifier-free Presburger arithmetic. J Autom Reason 47:341–367. doi:10.1007/s10817-011-9237-y
Cimatti A, Griggio A, Sebastiani R (2010) Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans Comput Log 12(1):7
Craig W (1957) Linear reasoning. A new form of the Herbrand–Gentzen theorem. J Symb Log 22(3):250–268
Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA, pp 443–456
Felsing D, Grebing S, Klebanov V, Rümmer P, Ulbrich M (2014) Automating regression verification. In: Crnkovic I, Chechik M, Grünbacher P (eds) ACM/IEEE international conference on automated software engineering, ASE. ACM, New York, pp 349–360
Fioravanti F, Pettorossi A, Proietti M, Senni V (2013) Generalization strategies for the verification of infinite state systems. TPLP 13(2):175–199. doi:10.1017/S1471068411000627
Godefroid P, Yannakakis M (2013) Analysis of boolean programs. In: TACAS, pp 214–229
Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: CAV
Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI
Gupta A, Popeea C, Rybalchenko A (2011) Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL
Gupta A, Popeea C, Rybalchenko A (2011) Solving recursion-free Horn clauses over LI+UIF. In: APLAS, pp 188–203
Gupta A, Popeea C, Rybalchenko A (2013) Generalised interpolation by solving recursion-free Horn clauses. CoRR abs/1303.7378
Hanus M (ed.) (2009) Logic-based program synthesis and transformation, 18th international symposium, LOPSTR 2008, Valencia, Spain, July 17–18, 2008, Revised Selected Papers, Lecture Notes in Computer Science, vol 5438. Springer, Berlin
Heizmann M, Hoenicke J, Podelski A (2010) Nested interpolants. In: POPL
Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: POPL. ACM, New York, pp 232–244
Hoder K, Bjørner N (2012) Generalized property directed reachability. In: SAT
Hojjat H, Iosif R, Konečný F, Kuncak V, Rümmer P (2012) Accelerating interpolants. In: Automated technology for verification and analysis (ATVA)
Jhala R, Majumdar R, Rybalchenko A (2011) HMC: Verifying functional programs using abstract interpreters. In: CAV
Kafle B, Gallagher JP (2014) Convex polyhedral abstractions, specialisation and property-based predicate splitting in Horn clause verification. In: Workshop on Horn clauses for verification and synthesis
Kincaid Z LIA Horn benchmarks. https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/LIA/Zachary/
Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Biere A, Bloem R (eds) CAV, Lecture Notes in Computer Science, vol 8559. Springer, Heidelberg, pp 17–34
Komuravelli A, Gurfinkel A, Chaki S, Clarke EM Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina and Veith [42], pp 846–862
Lal A, Qadeer S, Lahiri SK (2012) Corral: A solver for reachability modulo theories. In: CAV
McMillan KL iZ3 documentation. http://research.microsoft.com/en-us/um/redmond/projects/z3/iz3documentation.html
McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV
McMillan KL (2006) Lazy abstraction with interpolants. In: CAV
McMillan KL, Rybalchenko A (2013) Solving constrained Horn clauses using interpolation. Tech. Rep. MSR-TR-2013-6, Microsoft Research
Méndez-Lojo M, Navas JA, Hermenegildo MV (2007) A flexible, (C)LP-based approach to the analysis of object-oriented programs. In: LOPSTR, pp 154–168
Peralta JC, Gallagher JP, Saglam H (1998) Analysis of imperative programs through analysis of constraint logic programs. In: SAS
Rümmer P, Hojjat H, Kuncak V (2013) Classifying and solving Horn clauses for verification. In: VSTTE
Rümmer P, Hojjat H, Kuncak V (2013) Classifying and solving Horn clauses for verification. In: Cohen E, Rybalchenko A (eds.) VSTTE, Lecture Notes in Computer Science, vol 8164. Springer, Heidelberg, pp 1–21
Rümmer P, Hojjat H, Kuncak V Disjunctive interpolants for Horn-clause verification. In: Sharygina and Veith [42], pp 347–363
Rümmer P, Hojjat H, Kuncak V (2013) Disjunctive interpolants for Horn-Clause verification (Extended Technical Report). ArXiv e-prints (2013). http://arxiv.org/abs/1301.4973
Sery O, Fedyukovich G, Sharygina N (2011) Interpolation-based function summaries in bounded model checking. In: Haifa verification conference, pp 160–175
Sharygina N, Veith H (eds) (2013) Computer aided verification—25th international conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, Lecture Notes in Computer Science, vol 8044. Springer
Terauchi T (2010) Dependent types from counterexamples. In: POPL, pp 119–130
Unno H, Terauchi T, Kobayashi N (2013) Automating relatively complete verification of higher-order functional programs. In: POPL
Acknowledgments
We would like to thank Shaz Qadeer for discussions about the complexity of checking bounded recursive programs.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Rümmer, P., Hojjat, H. & Kuncak, V. On recursion-free Horn clauses and Craig interpolation. Form Methods Syst Des 47, 1–25 (2015). https://doi.org/10.1007/s10703-014-0219-7
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-014-0219-7