Formal Methods in System Design

, Volume 47, Issue 1, pp 1–25 | Cite as

On recursion-free Horn clauses and Craig interpolation



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.


Horn clause verification Interpolation Software verification SMT solver Software model checking Predicate abstraction 



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


  1. 1.
    Albarghouthi A, Gurfinkel A, Chechik M (2012) Craig interpretation. In: SASGoogle Scholar
  2. 2.
    Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI, pp 39–55Google Scholar
  3. 3.
    Ball T, Podelski, A, Rajamani SK (2002) Relative completeness of abstraction refinement for software model checking. In: TACAS’02, LNCS, vol 2280, p 158Google Scholar
  4. 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. 5.
    Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified Horn clauses. In: CAVGoogle Scholar
  6. 6.
    Beyer D (2014) Status report on software verification—(competition summary sv-comp 2014). In: TACAS, pp 373–388Google Scholar
  7. 7.
    Bjørner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified Horn clauses. In: SASGoogle Scholar
  8. 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 MATHCrossRefGoogle Scholar
  9. 9.
    Cimatti A, Griggio A, Sebastiani R (2010) Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans Comput Log 12(1):7MathSciNetCrossRefGoogle Scholar
  10. 10.
    Craig W (1957) Linear reasoning. A new form of the Herbrand–Gentzen theorem. J Symb Log 22(3):250–268MATHMathSciNetCrossRefGoogle Scholar
  11. 11.
    Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA, pp 443–456Google Scholar
  12. 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–360Google Scholar
  13. 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 MATHMathSciNetGoogle Scholar
  14. 14.
    Godefroid P, Yannakakis M (2013) Analysis of boolean programs. In: TACAS, pp 214–229Google Scholar
  15. 15.
    Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: CAVGoogle Scholar
  16. 16.
    Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDIGoogle Scholar
  17. 17.
    Gupta A, Popeea C, Rybalchenko A (2011) Predicate abstraction and refinement for verifying multi-threaded programs. In: POPLGoogle Scholar
  18. 18.
    Gupta A, Popeea C, Rybalchenko A (2011) Solving recursion-free Horn clauses over LI+UIF. In: APLAS, pp 188–203Google Scholar
  19. 19.
    Gupta A, Popeea C, Rybalchenko A (2013) Generalised interpolation by solving recursion-free Horn clauses. CoRR abs/1303.7378Google Scholar
  20. 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, BerlinGoogle Scholar
  21. 21.
    Heizmann M, Hoenicke J, Podelski A (2010) Nested interpolants. In: POPLGoogle Scholar
  22. 22.
    Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: POPL. ACM, New York, pp 232–244Google Scholar
  23. 23.
    Hoder K, Bjørner N (2012) Generalized property directed reachability. In: SATGoogle Scholar
  24. 24.
    Hojjat H, Iosif R, Konečný F, Kuncak V, Rümmer P (2012) Accelerating interpolants. In: Automated technology for verification and analysis (ATVA)Google Scholar
  25. 25.
    Jhala R, Majumdar R, Rybalchenko A (2011) HMC: Verifying functional programs using abstract interpreters. In: CAVGoogle Scholar
  26. 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 synthesisGoogle Scholar
  27. 27.
  28. 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–34Google Scholar
  29. 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–862Google Scholar
  30. 30.
    Lal A, Qadeer S, Lahiri SK (2012) Corral: A solver for reachability modulo theories. In: CAVGoogle Scholar
  31. 31.
  32. 32.
    McMillan KL (2003) Interpolation and SAT-based model checking. In: CAVGoogle Scholar
  33. 33.
    McMillan KL (2006) Lazy abstraction with interpolants. In: CAVGoogle Scholar
  34. 34.
    McMillan KL, Rybalchenko A (2013) Solving constrained Horn clauses using interpolation. Tech. Rep. MSR-TR-2013-6, Microsoft ResearchGoogle Scholar
  35. 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–168Google Scholar
  36. 36.
    Peralta JC, Gallagher JP, Saglam H (1998) Analysis of imperative programs through analysis of constraint logic programs. In: SASGoogle Scholar
  37. 37.
    Rümmer P, Hojjat H, Kuncak V (2013) Classifying and solving Horn clauses for verification. In: VSTTEGoogle Scholar
  38. 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–21Google Scholar
  39. 39.
    Rümmer P, Hojjat H, Kuncak V Disjunctive interpolants for Horn-clause verification. In: Sharygina and Veith [42], pp 347–363Google Scholar
  40. 40.
    Rümmer P, Hojjat H, Kuncak V (2013) Disjunctive interpolants for Horn-Clause verification (Extended Technical Report). ArXiv e-prints (2013).
  41. 41.
    Sery O, Fedyukovich G, Sharygina N (2011) Interpolation-based function summaries in bounded model checking. In: Haifa verification conference, pp 160–175Google Scholar
  42. 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. SpringerGoogle Scholar
  43. 43.
    Terauchi T (2010) Dependent types from counterexamples. In: POPL, pp 119–130Google Scholar
  44. 44.
    Unno H, Terauchi T, Kobayashi N (2013) Automating relatively complete verification of higher-order functional programs. In: POPLGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2014

Authors and Affiliations

  • Philipp Rümmer
    • 1
  • Hossein Hojjat
    • 2
  • Viktor Kuncak
    • 3
  1. 1.Department of Information TechnologyUppsala UniversityUppsalaSweden
  2. 2.Department of Computer ScienceCornell UniversityIthacaUSA
  3. 3.EPFL IC IIF LARALausanneSwitzerland

Personalised recommendations