MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica		dblp
dblp
Editor(s):
Cook, Byron
Podelski, Andreas		dblp
dblp
Not MPII Editor(s):
Cook, Byron
Podelski, Andreas
BibTeX cite key*:
Rybalchenko-Sofronie-vmcai07
Title, Booktitle
Title*:
Constraint Solving for Interpolation
Booktitle*:
8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007)
Event, URLs
Conference URL::
http://research.microsoft.com/vmcai07/
Downloading URL:
Event Address*:
Nice, France
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
14 January 2007
Event End Date:
16 January 2007
Publisher
Name*:
Springer
URL:
http://www.springer-ny.com/-
Address*:
-
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
??
Number:
Month:
Pages:
?
Year*:
2007
VG Wort Pages:
ISBN/ISSN:
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
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.
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort, CCL bibliography



BibTeX Entry:
@INPROCEEDINGS{Rybalchenko-Sofronie-vmcai07,
AUTHOR = {Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica},
 EDITOR = {Cook, Byron and Podelski, Andreas},
 TITLE = {Constraint Solving for Interpolation},
 BOOKTITLE = {8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007)},
 PUBLISHER = {Springer},
 YEAR = {2007},
 VOLUME = {??},
 PAGES = {?},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Nice, France},
}

Entry last modified by Viorica Sofronie-Stokkermans, 11/15/2006
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Viorica Sofronie-Stokkermans		Created
11/15/2006 01:44:49 PM
Revision
0.



Editor
Viorica Sofronie-Stokkermans



Edit Date
11/15/2006 01:44:49 PM