Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

Quantified Formulas; SMT; Tree Interpolation; Generic tree; Interpolants; Interpolation algorithms; Linear arithmetic; Literals; Quantified formula; Tree interpolation; Uninterpreted Functions; Theoretical Computer Science; Computer Science (all)

Abstract :

[en] We present a generic tree-interpolation algorithm in the SMT context with quantifiers. The algorithm takes a proof of unsatisfiability using resolution and quantifier instantiation and computes interpolants (which may contain quantifiers). Arbitrary SMT theories are supported, as long as each theory itself supports tree interpolation for its lemmas. In particular, we show this for the theory combination of equality with uninterpreted functions and linear arithmetic. The interpolants can be tweaked by virtually assigning each literal in the proof to interpolation partitions (colouring the literals) in arbitrary ways. The algorithm is implemented in SMTInterpol.

Disciplines :

Computer science

Author, co-author :

Henkel, Elisabeth ; University of Freiburg, Freiburg im Breisgau, Germany

Hoenicke, Jochen ; Certora, Tel Aviv-Yafo, Israel

Schindler, Tanja ; Université de Liège - ULiège > Montefiore Institute of Electrical Engineering and Computer Science

Language :

English

Title :

Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT

Publication date :

2023

Event name :

International Conference on Automated Deduction

Event place :

Rome, Italy

Event date :

01-07-2023 au 04-07-2023

Audience :

International

Main work title :

Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings

Editor :

Pientka, Brigitte

Publisher :

Springer Science and Business Media Deutschland GmbH

ISBN/EAN :

978-3-03-138498-1

Pages :

248–265

Additional URL :

https://link.springer.com/content/pdf/10.1007/978-3-031-38499-8_15

Funding text :

Acknowledgment. I thank Alexander Bentkamp, Stephan Schulz, Mark Summer-field, Petar Vukmirović, and Uwe Waldmann for textual suggestions. This research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant No. 713999, Matryoshka). This research has also received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).Partially funded by the Royal Society (International Exchanges, grant number IES\R2\212106)Over the years the work in this talk has been supported by the EPSRC, Leverhulme Trust, ERC, NSF, Cambridge Gates Foundation, Cambridge Trust.Research reported in this paper is partially funded by the EPSRC Fellowship ‘VeTSpec: Verified Trustworthy Software Specification’ (EP/R034567/1).Onderzoek – Vlaanderen (project G070521N) and by the EU ICT-48 2020 project TAILOR (GA 952215). Jakob Nordström was supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B. Andy Oertel was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.Acknowledgment. Thanks to the reviewers for their extensive constructive feedback and to Diego Olivier Fernandez Pons for introducing us to MIP pre-solving. The research was partially funded by the Austrian Science Fund (FWF) under project No. T-1306.Acknowledgments. We thank the reviewers for their helpful comments. The research reported here was funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – Projektnummer 465447331.Funded by the European Union (ERC, ExtenDD, project number: 101054714). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.This work was supported by the Research Training Group GRK 2428 CONVEY of the German Research Council (DFG).Jeremias Berg was fully supported by the Academy of Finland under grant 342145. Bart Bogaerts and Dieter Vandesande were supported by Fonds WetenschappelijkAcknowledgements. This work was partially supported by the National NaturalAcknowledgments. This work has been supported by the Czech Ministry of Education, Youth and Sports ERC.CZ project LL1908, and the FIT BUT internal project FIT-S-20-6427.Supported by JSPS KAKENHI Grant Number JP22K11900.Acknowledgments. This work was funded in part by NSF-BSF grant 2110397 (NSF) and 2020704 (BSF) and ISF grant number 619/21.Acknowledgements. This work has been partially funded by the Swedish Research Council (VR) under grant 2018-04727, the Swedish Foundation for Strategic Research (SSF) under the project WebSec (Ref. RIT17-0011), the Wallenberg project UPDATE, and the NSTC QC project under Grant no. NSTC 111-2119-M-001-004-and 112-2119-M-001-006-.Acknowledgements. This work is the result of a research internship hosted at TU Wien and defended at the University of Liège. The authors would like to thank Pascal Fontaine for valuable discussions and comments. We acknowledge funding from the ERC Consolidator Grant ARTIST 101002685 and the FWF SFB project SpyCoDe F8504.Acknowledgments. This project was funded in part by the Deutsche Forschungs-gemeinschaft (DFG) – 378803395 (ConVeY), an Alexander von Humboldt Professorship, and by the AFOSR under grant number FA9550-16-1-0288.Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) -235950644 (Project GI 274/6-2).

Available on ORBi :

since 08 March 2024

Statistics

Number of views

1 (0 by ULiège)

Number of downloads

1 (0 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

Bibliography

Blanc, R., Gupta, A., Kovács, L., Kragl, B.: Tree interpolation in vampire. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 173–181. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5 13
Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reason. 54(1), 69–97 (2015)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773 28
Christ, J., Hoenicke, J.: Instantiation-based interpolation for quantified formulae. In: Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, vol. 10161. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Germany (2010)
Christ, J., Hoenicke, J.: Proof tree preserving tree interpolation. J. Autom. Reasoning 57(1), 67–95 (2016)
Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31759-0 19
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. Formal Methods Syst. Des. 39(3), 246– 260 (2011)
Gleiss, B., Kovács, L., Suda, M.: Splitting proofs for interpolation. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 291–309. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5 18
Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL, pp. 331–344. ACM (2011)
Gurfinkel, A., Rollini, S.F., Sharygina, N.: Interpolation properties and SAT-based model checking. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 255–271. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8 19
Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: POPL, pp. 471– 482. ACM (2010)
Henkel, E., Hoenicke, J., Schindler, T.: Proof tree preserving sequence interpolation of quantified formulas in the theory of equality. In: SMT. CEUR Workshop Proceedings, vol. 2908, pp. 3–16. CEUR-WS.org (2021)
Henkel, E., Hoenicke, J., Schindler, T.: Choose your colour: tree interpolation for quantified formulas in SMT. CoRR abs/2305.11667 (2023). https://arxiv.org/abs/2305.11667
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232–244. ACM (2004)
Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: POPL, pp. 473–485. ACM (2017)
Kovács, L., Voronkov, A.: First-order interpolation and interpolating proof systems. In: LPAR. EPiC Series in Computing, vol. 46, pp. 49–64. EasyChair (2017)
McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2 2
McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3 31
Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361–382. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7 18
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997)
Rollini, S.F., Bruttomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 182–196. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19583-9 17
Rümmer, P., Hojjat, H., Kuncak, V.: On recursion-free horn clauses and Craig interpolation. Formal Methods Syst. Des. 47(1), 1–25 (2015)
Seghir, M.N., Podelski, A., Wies, T.: Abstraction refinement for quantified array assertions. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 3–18. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03237-0 3
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). https://doi.org/10.1007/11532231 26