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*:

8th International Conference on Verification, Model Checking and Abstract Interpretation (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*:

-

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
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
11/15/2006 01:44:49 PM
Revision
0.



Editor
Viorica Sofronie-Stokkermans



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



Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section