hide
Free keywords:
-
Abstract:
Interpolation is an important component of recent methods for
program verification. It provides a natural and effective means
for computing the separation between the sets of ‘good’ and
‘bad’ states. The existing algorithms for interpolant generation
are proof-based: They require explicit construction of proofs,
from which interpolants can be computed. Construction of such
proofs is a difficult task. We propose an algorithm for the
generation of interpolants for the combined theory of linear
arithmetic and uninterpreted function symbols that does not
require a priori constructed proofs to derive interpolants. It
uses a reduction of the problem to constraint solving in linear
arithmetic, which allows application of existing highly
optimized Linear Programming solvers in a black-box fashion.
We provide experimental evidence of the practical applicability
of our algorithm.
