Résumé | One of the main challenges in software verification is efficient and
precise compositional analysis of programs with procedures and loops.
Interpolation methods remain one of the most promising techniques for
such verification, and are closely related to solving Horn clause
constraints. In this talk, I introduce a new notion of interpolation,
disjunctive interpolation, which solves a more general class of
interpolation problems in one step, compared to previous notions of
interpolants, such as tree interpolants or inductive sequences of
interpolants. I present algorithms and complexity for construction of
disjunctive interpolants, as well as their use within an
abstraction-refinement loop. We have implemented Horn clause
verification algorithms that use disjunctive interpolants and evaluate
them on benchmarks expressed as Horn clauses over the theory of integer
linear arithmetic.
This talk presents joint work with Hossein Hojjat and Viktor Kuncak. |