Interpolation modulo theories

Hochschulschrift

Zusammenfassung: We present new concepts and techniques to generate interpolants from the proofs produced by SMT solvers. The overall result is to expand the scope of interpolation to the wealth of theories that are supported by SMT solvers. SMT solvers can prove satisfiability for an ever growing number of theories (and for their combinations; theories are often combined to account for rich data as commonly used in complex systems). However, according to the present state of the art, SMT solvers can compute interpolants only for a few selected theories (and it is unknown how two existing methods can be combined to compute interpolants in the combination of the theories). The notion of \emph{interpolant} goes back to Craig's interpolation theorem for first-order logic. An increasing range of software analysis tools use techniques based on interpolants.We present a new algorithm to compute Craig interpolants from the proof produced by an SMT solver, for a wide range of theories and for their combination. The algorithm uses the proof produced by the SMT solver but it does not interfere with the intermediate steps of producing the proof and it does not manipulate the proof. As a consequence, the algorithm is generic in the theory and it can be put on top of an existing SMT solver without impeding its generality and without impeding its efficiency.We also present an extension of the algorithm to tree interpolants. Tree interpolants are used whenever the behaviour of a software is not represented as a linear sequence (for example, to account for the return of a function call in the execution of a program). To our knowledge, this is the first algorithm that computes (provably correct) tree interpolants from SMT proofs. Motivated by the fact that interpolation algorithms without an existing correctness proof are notoriously wrong, we present a proof for the correctness of the tree interpolation algorithm.We show how one can instantiate the algorithm for the quantifier-free fragment of the theory of uninterpreted functions and the theory of linear arithmetic over the integers or the reals, and we have implemented the resulting algorithm. The implementation is part of the interpolating SMT solver SMTInterpol. It is freely available under LGPL. Feedback from users is encouraging

Object Details

• Location: Deutsche Nationalbibliothek Frankfurt am Main
• Extent: Online-Ressource
• Language: Englisch
• Notes: Albert-Ludwigs-Universität Freiburg, Dissertation, 2015

Classification and Topics

• Classification: Mathematik
• Keyword: Craig-Interpolation ; SMT Solver

Contributors, Places and Time

• Event: Veröffentlichung
• (where): Freiburg
• (who): Universität
• (when): 2015
• Creator: Christ, Jürgen
• Contributor: Podelski, Andreas

Further information

• DOI: 10.6094/UNIFR/10342
• URN: urn:nbn:de:bsz:25-freidok-103420
• Rights: Der Zugriff auf das Objekt ist unbeschränkt möglich.
• Last update: 25.03.2025, 1:55 PM CET