Abstract
Algorithms for computing Craig interpolants have several applications in program verification. Though different algorithms exist, the relationship between them and the properties of the interpolants they generate are not well understood. This paper is a study of interpolation algorithms for propositional resolution proofs. We show that existing interpolation algorithms are abstractions of a more general, parametrised algorithm. Further, existing algorithms reside in the coarsest abstraction that admits correct interpolation algorithms. The strength of interpolants constructed by existing interpolation algorithms and the variables they eliminate are analysed. The algorithms and their properties are formulated and analysed using abstract interpretation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Buss, S.R.: Propositional proof complexity: An introduction. In: Berger, U., Schwichtenberg, H. (eds.) Computational Logic. NATO ASI Series F: Computer and Systems Sciences, vol. 165, pp. 127–178. Springer, Heidelberg (1999)
Carbone, A.: Interpolants, cut elimination and flow graphs for the propositional calculus. Annals of Pure and Applied Logic 83(3), 249–299 (1997)
Cousot, P.: Abstract interpretation. MIT course 16.399 (February–May 2005)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages, pp. 269–282. ACM Press, New York (1979)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)
Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretations. In: Principles of Programming Languages, pp. 83–94. ACM Press, New York (1992)
Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. Journal of Symbolic Logic 22(3), 250–268 (1957)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) Verification, Model Checking and Abstract Interpretation. LNCS. Springer, Heidelberg (2010)
Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. Journal on Satisfiability, Boolean Modeling and Computation 5, 27–56 (2008); Special Issue on Constraints to Formal Verification
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. Journal of the ACM 47(2), 361–416 (2000)
Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 193–207. Springer, Heidelberg (2008)
Huang, G.: Constructing Craig interpolation formulas. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol. 959, pp. 181–190. Springer, Heidelberg (1995)
Kovács, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) Automated Deduction – CADE-22. LNCS, vol. 5663, pp. 199–213. Springer, Heidelberg (2009)
Krajíček, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic 62(2), 457–486 (1997)
Maehara, S.: On the interpolation theorem of Craig (in Japanese). Sûgaku 12, 235–237 (1961)
Mancosu, P. (ed.): Interpolations. Essays in Honor of William Craig. Synthese, vol. 164(3). Springer, Heidelberg (2008)
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)
Mundici, D.: Complexity of Craig’s interpolation. Fundamenta Informaticae 5, 261–278 (1982)
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic 62(3), 981–998 (1997)
Ranzato, F., Tapparo, F.: Generalizing the Paige-Tarjan algorithm by abstract interpretation. Information and Computation 206(5), 620–651 (2008)
Simmonds, J., Davies, J., Gurfinkel, A., Chechik, M.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. In: Formal Methods in Computer-Aided Design, pp. 3–12. IEEE Computer Society, Los Alamitos (2007)
Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
D’Silva, V. (2010). Propositional Interpolation and Abstract Interpretation. In: Gordon, A.D. (eds) Programming Languages and Systems. ESOP 2010. Lecture Notes in Computer Science, vol 6012. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11957-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-11957-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11956-9
Online ISBN: 978-3-642-11957-6
eBook Packages: Computer ScienceComputer Science (R0)