Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleConstraint solving for interpolation
Author(s) Andrey Rybalchenko, Viorica Sofronie-Stokkermans
TypeArticle in Journal
AbstractInterpolation 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.
KeywordsInterpolation, Constraint solving, Hierarchical reasoning, Program verification
URL http://www.sciencedirect.com/science/article/pii/S0747717110000854
JournalJournal of Symbolic Computation
Pages1212 - 1233
NoteSpecial Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops
Translation No
Refereed No