Philipp Rümmer: Domain-Specific Guidance for Craig Interpolation

Model checkers use abstractions to reduce the state space of software programs or hardware designs, either to speed up the verification process, or as a way of handling infinite state space. One of the most common methods to construct or refine abstractions is Craig interpolation, a logical tool to extract concise explanations for the (bounded) unreachability of error locations or states. To ensure rapid convergence, model checkers rely on theorem provers to find suitable interpolants, or interpolants containing the right predicates, in a generally infinite lattice of interpolants for any given interpolation problem.
We have recently presented a semantic framework for systematically exploring interpolant lattices, based on the notion of interpolation abstraction. Our approach is solver-independent and works by instrumenting the interpolation query, and therefore does not require any changes to the theorem prover. While simple to implement, interpolation abstractions are extremely flexible, and can incorporate domain-specific knowledge about promising interpolants, for instance in the form of interpolant templates used by the theorem prover. The framework can be used for a variety of logics, including arithmetic domains or programs operating on arrays or heap, and is also applicable for quantified interpolants. In this presentation, in particular the application to the analysis of software programs, and to (unbounded) Petri net models is considered.
The presentation is based on joint work with Jerome Leroux and Pavle Subotic, accepted for publication in Acta Informatica (to appear in 2015). Parts of the work were earlier presented at FMCAD 2013.