Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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

URL of the conference:

http://research.microsoft.com/vmcai07/

URL for downloading the paper:


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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section