Abstract
Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images or refine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL(\(\mathcal {T}\)) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N, Veith, H (eds.) Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pp. 313–329. Springer, Berlin (2013)
Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bjørner N, Voronkov, A (eds.) Proceedings of the 18th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 7180 of Lecture Notes in Artificial Intelligence, pp. 46–61. Springer, Berlin (2012)
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 129–179 (2009)
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003)
Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Larsen, K.G., Brinksma, E. (eds.) Proceedings of the 14th Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pp. 236–249. Springer, Berlin (2002)
Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak’s method for combining decision procedures. In: Armando, A. (ed.) Proceedings of the 4th Workshop on Frontiers of Combining Systems (FroCoS), volume 2309 of Lecture Notes in Computer Science. Springer, Berlin (2002)
Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) Proceedings of the 20th Conference on Computer Aided Verification (CAV), volume 5123 of Lecture Notes in Computer Science, pp. 304–308. Springer, Berlin (2008)
Bonacina, M.P.: On theorem proving for program checking – historical perspective and recent developments. In: Fernandez, M. (ed.) Proceedings of the 12th International Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 1–11. ACM, New York (2010)
Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Trans. Comput. Log. 8(1), 180–208 (2007)
Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. In: Cook, B., Sebastiani, R. (eds.) Proceedings of the 4th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006), volume 174(8) of Electronic Notes in Theoretical Computer Science, pp. 55–70. Elsevier, Amsterdam (2007)
Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial \(\mathcal {T}\)-satisfiability procedures. J. Log. Comput. 18(1), 77–96 (2008)
Bonacina, M.P., Hsiang, J.: On the modelling of search in theorem proving – towards a theory of strategy analysis. Inf. Comput. 147, 171–208 (1998)
Bonacina, M.P., Johansson, M.: On interpolation in decision procedures. In: Brünnler, K., Metcalfe, G. (eds.) Proceedings of the 20th International Conference on Analytic Tableaux and Related Methods (TABLEAUX), volume 6793 of Lecture Notes in Artificial Intelligence, pp. 1–16. Springer, Berlin (2011)
Bonacina, M.P., Johansson, M.: Towards interpolation in an SMT solver with integrated superposition. In: Lahiri, S., Seshia, S. A. (eds.) Notes of the 9th International Workshop on Satisfiability Modulo Theories (SMT), number UCB/EECS-2011-80 in Technical Reports, pp. 9–18. Department of EECS, University of California at Berkeley, Berkeley (2011)
Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reason. 54(1), 69–97 (2015)
Bradley, A.R., Manna, Z.: The calculus of computation – decision procedures with applications to verification. Springer, Berlin (2007)
Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Giesl, J., Hähnle, R. (eds.) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 384–399. Springer, Berlin (2010)
Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: Program verification via Craig interpolation for Presburger arithmetic with arrays. Notes of the 6th International Verification Workshop (VERIFY), 2010. Available at http://www.philipp.ruemmer.org/
Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In: Jhala, R., Schmidt, D. (eds.) Proceedings of the 12th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), volume 6538 of Lecture Notes in Computer Science, pp. 88–102. Springer, Berlin (2011)
Bruttomesso, R., Ghilardi, S., Ranise, S.: A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Proceedings of the 8th Symposium on Frontiers of Combining Systems (FroCoS), volume 6989 of Lecture Notes in Artificial Intelligence, pp. 103–118. Springer, Berlin (2011)
Bruttomesso, R., Ghilardi, S., Ranise, S.: From strong amalgamability to modularity of quantifier-free interpolation. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), volume 7364 of Lecture Notes in Artificial Intelligence, pp. 118–133. Springer, Berlin (2012)
Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation for a theory of arrays. Logical Methods Comput. Sci. 8(2) (2012)
Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1) (2014)
Bruttomesso, R., Rollini, S.F., Sharygina, N., Tsitovich, A.: Flexible interpolation generation in satisfiability modulo theories. In: Proceedings of the 14th International Conference on Computer-Aided Design (ICCAD), pp. 770–777. IEEE, Los Alamitos (2010)
Christ, J., Hoenicke, J.: Instantiation-based interpolation for quantified formulae. Notes of the 8th International Workshop on Satisfiability Modulo Theories (SMT) (2010)
Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), Article 7 (2010)
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)
Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250–268 (1957)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. ACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)
de Moura, L., Bjørner, N.: Efficient E-matching for SMT-solvers. In: Pfenning, F. (ed.) Proceedings of the 21st Conference on Automated Deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence, pp. 183–198. Springer, Berlin (2007)
de Moura, L., Bjørner, N.: Bugs, moles and skeletons: Symbolic reasoning for software development. In: Giesl, J., Hähnle, R. (eds.) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 400–411. Springer, Berlin (2010)
de Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Comm. ACM 54(9), 69–77 (2011)
Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of automated reasoning, vol. 1, pp. 535–610. Elsevier, Amsterdam (2001)
Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
D’Silva, V.: Propositional interpolation and abstract interpretation. In: Gordon, A.D. (ed.) Proceedings of the 19th European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pp. 185–204. Springer, Berlin (2010)
D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M.V. (eds.) Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 5944 of Lecture Notes in Computer Science, pp. 129–145. Springer, Berlin (2010)
Fitting, M.: First-order logic and automated theorem proving. Springer, Berlin (1996)
Fuchs, A., Goel, A., Grundy, J., Krstić, S., Tinelli, C.: Ground interpolation for the theory of equality. Logical Methods Comput. Sci. 8(1) (2012)
Gallier, J.: Logic for computer science – foundations of automatic theorem proving. Wiley, New York (1987)
Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 240(10), 1453–1492 (2006)
Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) Proceedings of the 21st conference on automated deduction (CADE), volume 4603 of Lecture Notes in Artificial Intelligence, pp. 167–182. Springer, Berlin (2007)
Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani, A., Maler, O. (eds.) Proceedings of the 21st conference on computer aided verification (CAV), volume 5643 of Lecture Notes in Computer Science, pp. 306–320. Springer, Berlin (2009)
Givan, R., McAllester, D.: Proceedings of the 3rd international conference on principles of knowledge representation and reasoning (KR). In: Nebel, B., Rich, C., Swartout, W. R. (eds.) , pp. 403–412. Morgan Kaufmann (1992)
Goel, A., Krstić, S., Tinelli, C.: Ground interpolation for combined theories. In: Schmidt, R. (ed.) Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 183–198. Springer, Berlin (2009)
Griggio, A.: Effective word-level interpolation for software verification. In: Bjesse, P., Slobodova, A. (eds.) Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE, New York (2011)
Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free Horn clauses over LI+UIF. In: Yang, H. (ed.) Proceedings of the 9th Asian Symposium on Programming Languages and Systems (APLAS), volume 7078 of Lecture Notes in Computer Science. Springer, Berlin (2011)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Leroy, X. (ed.) Proceedings of the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 232–244. ACM, New York (2004)
Hoder, K., Kovàcs, L., Voronkov, A.: Interpolation and symbol elimination in Vampire. In: Giesl, J., Hähnle, R. (eds.) Proceedings of the 5th international joint conference on automated reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 188–195. Springer, Berlin (2010)
Hoder, K., Kovàcs, L., Voronkov, A.: Playing in the grey area of proofs. In: Hicks, M. (ed.) Proceedings of the 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pp. 259–272. ACM, New York (2012)
Huang, G.: Constructing Craig interpolation formulas. In: Du, D.-Z., Li, M. (eds.) Proceedings of the 1st Annual International Conference on Computing and Combinatorics (COCOON), volume 959 of Lecture Notes in Computer Science, pp. 181–190. Springer, Berlin (1995)
Jain, H.: Verification using satisfiability checking, predicate abstraction and Craig interpolation. PhD thesis, School of Computer Science, Carnegie Mellon University (2008)
Kapur, D., Majumdar, R., Zarba, C.G., et al.: Interpolation for data structures. In: Devambu, P. (ed.) Proceedings of the 14th ACM SIGSOFT Symposium on the Foundations of Software Engineering. ACM Press (2006)
Kleene, S.C.: Mathematical logic. Wiley Interscience, New York (1967)
Kovàcs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R. (ed.) Proceedings of the 22nd Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 199–213. Springer, Berlin (2009)
Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log. 62(2), 457–486 (1997)
Krajíček, J., Pudlàk, P.: Some consequences of cryptographical conjectures for \({s^{1}_{2}}\) and EF. Inf. Comput. 140, 82–94 (1998)
Kroening, D., Weissenbacher, G.: Lifting propositional interpolants to the word-level. In: Baumgartner, J., Sheeran, M. (eds.) Proceedings of the 7th Conference on Formal Methods in Computer Aided Design (FMCAD), pp. 85–89. ACM and IEEE, New York (2007)
Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qaader, S. (eds.) Proceedings of the 23rd Conference on Computer Aided Verification (CAV), volume 6806 of Lecture Notes in Computer Science, pp. 573–578. Springer, Berlin (2011)
Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) Proceedings of the 14th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 4790 of Lecture Notes in Artificial Intelligence, pp. 348–362. Springer, Berlin (2007)
Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Comm. ACM 52(8), 76–82 (2009)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE/ACM International Conference on Computer Aided Design (ICCAD), pp. 220–227 (1997)
McAllester, D.: Automatic recognition of tractability in inference relations. J. ACM 40(2), 284–303 (1993)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Proceedings of the 15th Conference on Computer Aided Verification (CAV), volume 2725 of Lecture Notes in Computer Science, pp. 1–13. Springer, Berlin (2003)
McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005)
McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R. B. (eds.) Proceedings of the 18th Conference on Computer Aided Verification (CAV), volume 4144 of Lecture Notes in Computer Science, pp. 123–136. Springer, Berlin (2006)
McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C. R., Rehof, J. (eds.) Proceedings of the 14th Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pp. 413–427. Springer, Berlin (2008)
McMillan, K.L.: Lazy annotation for program testing and verification. In: Proceedings of the 22nd Conference on Computer Aided Verification (CAV), volume 6174 of Lecture Notes in Computer Science, pp. 104–118. Springer, Berlin (2010)
McMillan, K.L.: Interpolants from Z3 proofs. In: Bjesse, P., Slobodova, A. (eds.) Proceedings of the 11th Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE, New York (2011)
Moskał, M.: Fx7 or in software, it is all about quantifiers. System Descriptions at the Satisfiability Modulo Theories Competition (SMT-COMP) (2007). Available at http://research.microsoft.com/en-us/um/people/moskal/
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Blaauw, D., Lavagno, L. (eds.) Proceedings of the 39th Design Automation Conference (DAC), pp. 530–535 (2001)
Mundici, D.: Complexity of Craig’s interpolation. Fundamenta Informaticae 5, 261–278 (1982)
Nelson, G.: Techniques for Program Verification. PhD thesis, Stanford University, 1979. A revised version was published as Xerox PARC Computer Science Laboratory Research Report No. CSL-81-10
Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W. W., Loveland, D. W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201–211. American Mathematical Society (1983)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)
Pudlàk, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic 62(3), 981–998 (1997)
Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: Parthasarathy, M., Seshia, S. A. (eds.) Proceedings of the 24th Conference on Computer Aided Verification (CAV), volume 7358 of Lecture Notes in Computer Science, pp. 193–209. Springer, Berlin (2012)
Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolation for Horn clause verification. In: Sharygina, N., Veith, H. (eds.) Proceedings of the 25th Conference on Computer Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pp. 347–363. Springer, Berlin (2013)
Rümmer, P., Subotić, P.: Exploring interpolants. In: Jobstmann, B., Ray, S. (eds.) Proceedings of the 13th Conference on Formal Methods in Computer Aided Design (FMCAD). FMCAD Inc (2013)
Shankar, N.: Automated deduction for verification. ACM Comput. Surv. 41(4), 40–96 (2009)
Smullyan, R.M.: First-order logic. Dover Publications, New York (1995). First published by Springer in 1968
Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods in Computer Science 4(4), Article 1 (2008)
Takeuti, G.: Proof theory, volume 81 of studies in logic. North Holland, Amsterdam (1975)
Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1, 425–467 (1995)
Weissenbacher, G.: Program Analysis with Interpolants. PhD thesis, Magdalen College, Oxford University (2010)
Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. Technical Report MSR-TR-2004-108, Microsoft Research (2004)
Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) Proceedings of the 20th Conference on Automated Deduction (CADE), volume 3632 of Lecture Notes in Artificial Intelligence, pp. 353–368. Springer, Berlin (2005)
Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE), pp. 10880–10885. IEEE, Los Alamitos (2003)
Author information
Authors and Affiliations
Corresponding author
Additional information
Research supported in part by grant no. 2007-9E5KM8 of the Ministero dell’Istruzione Università e Ricerca, Italy, and by COST Action IC0901 Rich-model Toolkit of the European Union.
Rights and permissions
About this article
Cite this article
Bonacina, M.P., Johansson, M. Interpolation Systems for Ground Proofs in Automated Deduction: a Survey. J Autom Reasoning 54, 353–390 (2015). https://doi.org/10.1007/s10817-015-9325-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9325-5