English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

Constraint Solving for Interpolation

MPS-Authors
/persons/resource/persons45328

Rybalchenko,  Andrey
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45516

Sofronie-Stokkermans,  Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Rybalchenko, A., & Sofronie-Stokkermans, V. (2010). Constraint Solving for Interpolation. Journal of Symbolic Computation, 45(11), 1212-1233. doi:101016/j.jsc.2010.06.005.


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-14AA-F
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.