Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

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

Action:

login to update

Options:




Library Locked Library locked




Author, Editor(s)

Author(s):

Rybalchenko, Andrey
Sofronie-Stokkermans, Viorica

dblp
dblp

Not MPG Author(s):

Rybalchenko, Andrey

BibTeX cite key*:

Sofronie-Stokkermans-2010-jsc

Title

Title*:

Constraint Solving for Interpolation

Journal

Journal Title*:

Journal of Symbolic Computation

Journal's URL:

http://www.elsevier.com/wps/find/journaldescription.cws_home/622902/description#description

Download URL
for the article:

http://www.sciencedirect.com/science/article/B6WM7-50C71T0-3/2/4b391bab5e3621ac8fc979af3874cbaf

Language:

English

Publisher

Publisher's
Name:

Elsevier

Publisher's URL:

http://www.elsevier.com/

Publisher's
Address:

Amsterdam

ISSN:

0747-7171

Vol, No, pp, Date

Volume*:

45

Number:

11

Publishing Date:

2010

Pages*:

1212-1233

Number of
VG Pages:


Page Start:

1212

Page End:

1233

Sequence Number:


DOI:

101016/j.jsc.2010.06.005

Note, Abstract, ©

Note:


(LaTeX) Abstract:

Interpolation is an important component of recent methods for
program verification. It provides a natural and effective means
for computing the 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 a black-box fashion.
We provide experimental evidence of the practical applicability
of our algorithm.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:

@ARTICLE{Sofronie-Stokkermans-2010-jsc,
AUTHOR = {Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica},
TITLE = {Constraint Solving for Interpolation},
JOURNAL = {Journal of Symbolic Computation},
PUBLISHER = {Elsevier},
YEAR = {2010},
NUMBER = {11},
VOLUME = {45},
PAGES = {1212--1233},
ADDRESS = {Amsterdam},
ISBN = {0747-7171},
DOI = {101016/j.jsc.2010.06.005},
}


Entry last modified by Anja Becker, 03/15/2011
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)
[Library]
Created
02/26/2010 01:28:12 PM
Revisions
3.
2.
1.
0.
Editor(s)
Anja Becker
Anja Becker
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
15.03.2011 09:56:26
19.01.2011 14:59:03
09/10/2010 02:20:05 PM
02/26/2010 01:28:12 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section