×

On recursion-free Horn clauses and Craig interpolation. (English) Zbl 1322.68134

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03C40 Interpolation, preservation, definability

Software:

HMC; Spacer; Princess
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Albarghouthi A, Gurfinkel A, Chechik M (2012) Craig interpretation. In: SAS
[2] Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI, pp 39-55 · Zbl 1325.68137
[3] Ball T, Podelski, A, Rajamani SK (2002) Relative completeness of abstraction refinement for software model checking. In: TACAS’02, LNCS, vol 2280, p 158 · Zbl 1043.68523
[4] 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 · Zbl 1185.68406
[5] Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified Horn clauses. In: CAV · Zbl 1482.68134
[6] Beyer D (2014) Status report on software verification—(competition summary sv-comp 2014). In: TACAS, pp 373-388
[7] Bjørner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified Horn clauses. In: SAS
[8] 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 · Zbl 1259.03043
[9] Cimatti A, Griggio A, Sebastiani R (2010) Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans Comput Log 12(1):7 · Zbl 1351.68247
[10] Craig W (1957) Linear reasoning. A new form of the Herbrand-Gentzen theorem. J Symb Log 22(3):250-268 · Zbl 0081.24402
[11] Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA, pp 443-456 · Zbl 1381.68057
[12] 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
[13] 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 · Zbl 1267.68080
[14] Godefroid P, Yannakakis M (2013) Analysis of boolean programs. In: TACAS, pp 214-229 · Zbl 1381.68164
[15] Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: CAV
[16] Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI · Zbl 1267.68080
[17] Gupta A, Popeea C, Rybalchenko A (2011) Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL · Zbl 1284.68427
[18] Gupta A, Popeea C, Rybalchenko A (2011) Solving recursion-free Horn clauses over LI+UIF. In: APLAS, pp 188-203 · Zbl 1351.68247
[19] Gupta A, Popeea C, Rybalchenko A (2013) Generalised interpolation by solving recursion-free Horn clauses. CoRR abs/1303.7378 · Zbl 1464.68204
[20] 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
[21] Heizmann M, Hoenicke J, Podelski A (2010) Nested interpolants. In: POPL · Zbl 1312.68059
[22] Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: POPL. ACM, New York, pp 232-244 · Zbl 1325.68147
[23] Hoder K, Bjørner N (2012) Generalized property directed reachability. In: SAT · Zbl 1273.68229
[24] Hojjat H, Iosif R, Konečný F, Kuncak V, Rümmer P (2012) Accelerating interpolants. In: Automated technology for verification and analysis (ATVA) · Zbl 1374.68291
[25] Jhala R, Majumdar R, Rybalchenko A (2011) HMC: Verifying functional programs using abstract interpreters. In: CAV
[26] 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 · Zbl 1464.68208
[27] Kincaid Z LIA Horn benchmarks. https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/LIA/Zachary/
[28] 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 · Zbl 1358.68072
[29] 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
[30] Lal A, Qadeer S, Lahiri SK (2012) Corral: A solver for reachability modulo theories. In: CAV
[31] McMillan KL iZ3 documentation. http://research.microsoft.com/en-us/um/redmond/projects/z3/iz3documentation.html · Zbl 1351.68247
[32] McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV · Zbl 1278.68184
[33] McMillan KL (2006) Lazy abstraction with interpolants. In: CAV · Zbl 1188.68196
[34] McMillan KL, Rybalchenko A (2013) Solving constrained Horn clauses using interpolation. Tech. Rep. MSR-TR-2013-6, Microsoft Research
[35] 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 · Zbl 1179.68030
[36] Peralta JC, Gallagher JP, Saglam H (1998) Analysis of imperative programs through analysis of constraint logic programs. In: SAS
[37] Rümmer P, Hojjat H, Kuncak V (2013) Classifying and solving Horn clauses for verification. In: VSTTE · Zbl 1322.68134
[38] 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 · Zbl 1322.68134
[39] Rümmer P, Hojjat H, Kuncak V Disjunctive interpolants for Horn-clause verification. In: Sharygina and Veith [42], pp 347-363
[40] 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
[41] Sery O, Fedyukovich G, Sharygina N (2011) Interpolation-based function summaries in bounded model checking. In: Haifa verification conference, pp 160-175
[42] 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 · Zbl 1268.68032
[43] Terauchi T (2010) Dependent types from counterexamples. In: POPL, pp 119-130 · Zbl 1312.68041
[44] Unno H, Terauchi T, Kobayashi N (2013) Automating relatively complete verification of higher-order functional programs. In: POPL · Zbl 1301.68182
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.