Skip to main content
SpringerLink
Log in

On recursion-free Horn clauses and Craig interpolation

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8

Similar content being viewed by others

Notes

  1. The concept of auxiliary Boolean variables to represent interpolation problems has also been used in [41] and [2], for the purpose of extracting function summaries in model checking.

  2. http://lara.epfl.ch/w/eldarica.

  3. http://z3.codeplex.com, version 4.3.2.

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

  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

  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

  5. Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified Horn clauses. In: CAV

  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

    Article  MATH  Google Scholar 

  9. Cimatti A, Griggio A, Sebastiani R (2010) Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans Comput Log 12(1):7

    Article  MathSciNet  Google Scholar 

  10. Craig W (1957) Linear reasoning. A new form of the Herbrand–Gentzen theorem. J Symb Log 22(3):250–268

    Article  MATH  MathSciNet  Google Scholar 

  11. Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA, pp 443–456

  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

    MATH  MathSciNet  Google Scholar 

  14. Godefroid P, Yannakakis M (2013) Analysis of boolean programs. In: TACAS, pp 214–229

  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

  17. Gupta A, Popeea C, Rybalchenko A (2011) Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL

  18. Gupta A, Popeea C, Rybalchenko A (2011) Solving recursion-free Horn clauses over LI+UIF. In: APLAS, pp 188–203

  19. Gupta A, Popeea C, Rybalchenko A (2013) Generalised interpolation by solving recursion-free Horn clauses. CoRR abs/1303.7378

  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

  22. Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: POPL. ACM, New York, pp 232–244

  23. Hoder K, Bjørner N (2012) Generalized property directed reachability. In: SAT

  24. Hojjat H, Iosif R, Konečný F, Kuncak V, Rümmer P (2012) Accelerating interpolants. In: Automated technology for verification and analysis (ATVA)

  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

  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

  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

  32. McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV

  33. McMillan KL (2006) Lazy abstraction with interpolants. In: CAV

  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

  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

  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

  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

  43. Terauchi T (2010) Dependent types from counterexamples. In: POPL, pp 119–130

  44. Unno H, Terauchi T, Kobayashi N (2013) Automating relatively complete verification of higher-order functional programs. In: POPL

Download references

Acknowledgments

We would like to thank Shaz Qadeer for discussions about the complexity of checking bounded recursive programs.

Author information

Authors and Affiliations

  1. Department of Information Technology, Uppsala University, Box 337, 75105, Uppsala, Sweden

    Philipp Rümmer

  2. Department of Computer Science, Cornell University, 442 Gates Hall, Ithaca, NY, 14853, USA

    Hossein Hojjat

  3. EPFL IC IIF LARA, Station 14, 1015, Lausanne, Switzerland

    Viktor Kuncak

Authors
  1. Philipp Rümmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hossein Hojjat
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Viktor Kuncak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hossein Hojjat.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

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

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-014-0219-7

Keywords

Search

Navigation