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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

Constraint Solving for Interpolation

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

Rybalchenko,  Andrey
Programming Logics, 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;
Programming Logics, 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. (2007). Constraint Solving for Interpolation. In B. Cook, & A. Podelski (Eds.), Verification, Model Checking and Abstract Interpretation: 8th International Conference, VMCAI 2007 (pp. 346-362). Berlin, Germany: Springer.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-1EB9-1
Zusammenfassung
Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing 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 black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.