de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Constraint Solving for Interpolation

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45328

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

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45516

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-14AA-F
Zusammenfassung
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.