Abstract
As a promising direction to overcome difficulties of verification, researchers have recently proposed the use of Horn constraints as intermediate representation. Horn constraints are related to Craig interpolation, which is one of the main techniques used to construct and refine abstractions in verification, and to synthesise inductive loop invariants. We give a classification of the different forms of Craig interpolation problems found in literature, and show that all of them correspond to natural fragments of (recursion-free) Horn constraints. For a logic that has the binary interpolation property, all of these problems are solvable, but have different complexity. In addition to presenting the theoretical classification and solvability results, we present a publicly available collection of benchmarks to evaluate solvers for Horn constraints, categorized according to our classification. The benchmarks are derived from real-world verification problems. The behavior with our tools as well as with Z3 prover indicates the importance of Horn clause solving as distinct from the general problem of solving quantified constraints by quantifier instantiation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Albarghouthi, A., Gurfinkel, A., Chechik, M.: Craig interpretation. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 300–316. Springer, Heidelberg (2012)
Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: An interpolation-based algorithm for inter-procedural verification. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 39–55. Springer, Heidelberg (2012)
Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672–678. Springer, Heidelberg (2012)
Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 158–172. Springer, Heidelberg (2002)
Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: Version 2.0. Technical report (2010)
Bjørner, N., McMillan, K., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT Workshop at IJCAR (2012)
Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving (2012) (submitted)
Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. Journal of Automated Reasoning 47, 341–367 (2011)
Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), 7 (2010)
Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic 22(3), 250–268 (1957)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465–476 (1979)
Fermüller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 25, pp. 1791–1850. Elsevier (2001)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV 1997, pp. 72–83 (1997)
Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)
Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL (2011)
Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free Horn clauses over LI+UIF. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 188–203. Springer, Heidelberg (2011)
Gupta, A., Popeea, C., Rybalchenko, A.: Generalised interpolation by solving recursion-free horn clauses. CoRR, abs/1303.7378 (2013)
Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL (2010)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232–244. ACM (2004)
Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012)
Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012)
Lewis, H.R.: Renaming a set of clauses as a Horn set. J. ACM 25(1), 134–135 (1978)
McMillan, K.L.: iZ3 documentation, http://research.microsoft.com/en-us/um/redmond/projects/z3/iz3documentation.html
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
McMillan, K.L.: Applications of craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005)
McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
McMillan, K.L., Rybalchenko, A.: Solving constrained Horn clauses using interpolation. Technical Report MSR-TR-2013-6 (January 2013), http://research.microsoft.com/apps/pubs/default.aspx?id=180055
Méndez-Lojo, M., Navas, J.A., Hermenegildo, M.V.: A flexible (c)lp-based approach to the analysis of object-oriented programs. In: King, A. (ed.) LOPSTR 2007. LNCS, vol. 4915, pp. 154–168. Springer, Heidelberg (2008)
Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report). ArXiv e-prints (January 2013), http://arxiv.org/abs/1301.4973
Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 160–175. Springer, Heidelberg (2012)
Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011)
Taghdiri, M., Jackson, D.: Inferring specifications to detect errors in code. Autom. Softw. Eng. 14(1), 87–121 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rümmer, P., Hojjat, H., Kuncak, V. (2014). Classifying and Solving Horn Clauses for Verification. In: Cohen, E., Rybalchenko, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2013. Lecture Notes in Computer Science, vol 8164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54108-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-54108-7_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54107-0
Online ISBN: 978-3-642-54108-7
eBook Packages: Computer ScienceComputer Science (R0)