MPI-INF Logo
Publications

Server    domino.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*:
Verification, Model Checking and Abstract Interpretation : 8th International Conference, 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*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
4349
Number:
Month:
Pages:
346-362
Year*:
2007
VG Wort Pages:
28
ISBN/ISSN:
978-3-540-69735-0
Sequence Number:
DOI:
10.1007/978-3-540-69738-1_25
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:
popular
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



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 = {Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007},
PUBLISHER = {Springer},
YEAR = {2007},
VOLUME = {4349},
PAGES = {346--362},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Nice, France},
ISBN = {978-3-540-69735-0},
DOI = {10.1007/978-3-540-69738-1_25},
}


Entry last modified by Viorica Sofronie-Stokkermans, 02/28/2008
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
03/12/2007 10:44:25 AM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Christine Kiesel
Christine Kiesel
Edit Dates
01/07/2008 03:41:59 PM
01/07/2008 03:30:33 PM
01/07/2008 02:23:30 PM
12.07.2007 11:42:00
12.07.2007 10:49:40