Abstract
Craig interpolation has a wide range of applications in model checking, verification, and state space abstraction. Recent advances use a more general version of interpolation called tree interpolation. In this paper, we present a method to extract tree interpolants from a proof tree generated by an SMT solver without modifying the proof tree. The framework is general with respect to the theories involved. We instantiate the framework to the combination of the theories of uninterpreted functions and linear arithmetic.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: CAV, pp. 313–329. Springer, Berlin (2013)
Blanc, R., Gupta, A., Kovács, L., Kragl, B.: Tree interpolation in vampire. In: LPAR, pp. 173–181. Springer, Berlin (2013)
Brillout, A., Kroening, D., Rümmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: IJCAR, pp. 384–399 (2010)
Bruttomesso, R., Ghilardi, S., Ranise, S.: From strong amalgamability to modularity of quantifier-free interpolation. In: IJCAR’12, pp. 118–133 (2012)
Bruttomesso, R., Rollini, S., Sharygina, N., Tsitovich, A.: Flexible interpolation with local proof transformations. In: ICCAD, pp. 770–777 (2010)
Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: SPIN’12, pp. 248–254. Springer, Berlin (2012)
Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: TACAS’13, pp. 124–138. Springer, Berlin (2013)
Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. Reports of SFB/TR 14 AVACS 89, SFB/TR 14 AVACS, February 2013. ISSN: 1860–9821. http://www.avacs.org
Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: TACAS’08, pp. 397–412. Springer, Berlin (2008)
Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269–285 (1957)
Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV’09, pp. 233–247 (2009)
Dräger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: a certifying model checker for infinite-state concurrent systems. In: TACAS’10, pp. 271–274. Springer, Brlin (2010)
D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: VMCAI’10, pp. 129–145 (2010)
Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV’06, pp. 81–94. Springer, Berlin (2006)
Farzan, A., Kincaid, Z., Podelski, A.: Inductive data flow graphs. In: POPL’13, pp. 129–142. ACM, New york (2013)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): sast decision procedures. In: CAV’04, pp. 175–188 (2004)
Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free horn clauses over LI+UIF. In: APLAS’11, pp. 188–203. Springer, Berlin (2011)
Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In POPL’10, pp. 471–482. ACM, New York (2010)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL’04, pp. 232–244. Springer, Berlin (2004)
King, T., Barrett, C., Dutertre, B.: Simplex with sum of infeasibilities for SMT. In: FMCAD’13, pp. 189–196 (2013)
McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV’03, 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: CAV’06, pp. 123–136. Springer, Berlin (2006)
McMillan, K.L.: Interpolants from Z3 proofs. In: FMCAD, pp. 19–27. Springer, Berlin (2011)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997)
Rümmer, P., Hojjat, H., Kuncak, V.: Classifying and solving horn clauses for verification. In VSTTE, pp. 1–21. Springer, Berlin (2013)
Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: FMCAD’12, pp. 114–121. IEEE, New York (2012)
Totla, N., Wies, T.: Complete instantiation-based interpolation. In: POPL, pp. 537–548. ACM, New York (2013)
Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: CADE, pp. 353–368 (2005)
Author information
Authors and Affiliations
Corresponding author
Additional information
This work is supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR14 AVACS).
Rights and permissions
About this article
Cite this article
Christ, J., Hoenicke, J. Proof Tree Preserving Tree Interpolation. J Autom Reasoning 57, 67–95 (2016). https://doi.org/10.1007/s10817-016-9365-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-016-9365-5