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:




Library Locked Library locked




Author, Editor

Author(s):

Jacobs, Swen

dblp



Editor(s):

Bouajjani, Ahmed
Maler, Oded

dblp
dblp

Not MPII Editor(s):

Bouajjani, Ahmed
Maler, Oded

BibTeX cite key*:

Jacobs2009

Title, Booktitle

Title*:

Incremental Instance Generation in Local Reasoning


IIGLR.pdf (208.95 KB)

Booktitle*:

Computer Aided Verification : 21st International Conference, CAV 2009

Event, URLs

URL of the conference:

http://www-cav2009.imag.fr

URL for downloading the paper:

http://dx.doi.org/10.1007/978-3-642-02658-4_29

Event Address*:

Grenoble, France

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

29 June 2009

Event End Date:

2 July 2009

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

5643

Number:


Month:

June

Pages:

368-382

Year*:

2009

VG Wort Pages:


ISBN/ISSN:

978-3-642-02657-7

Sequence Number:


DOI:

10.1007/978-3-642-02658-4_29



Note, Abstract, ©


(LaTeX) Abstract:

Many verification approaches use SMT solvers in some form, and are limited by
their incomplete handling of quantified formulas. Local reasoning allows to
handle SMT problems involving a certain class of
universally quantified formulas in a complete way by instantiation to a finite
set of ground formulas. We present a method to generate these instances
incrementally, in order to provide a more efficient way of solving these
satisfiability problems. The incremental instantiation is guided semantically,
inspired by the instance generation approach to first-order theorem proving. Our
method is sound and complete, and terminates on both satisfiable and
unsatisfiable input after generating a subset of the instances needed in
standard local reasoning. Experimental results show that for a large class of
examples the incremental approach is substantially more efficient than eager
generation of all instances.

Keywords:

Local Reasoning, Instance Generation, SMT, Quantifiers, Theory Extensions



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:

@INPROCEEDINGS{Jacobs2009,
AUTHOR = {Jacobs, Swen},
EDITOR = {Bouajjani, Ahmed and Maler, Oded},
TITLE = {Incremental Instance Generation in Local Reasoning},
BOOKTITLE = {Computer Aided Verification : 21st International Conference, CAV 2009},
PUBLISHER = {Springer},
YEAR = {2009},
VOLUME = {5643},
PAGES = {368--382},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Grenoble, France},
MONTH = {June},
ISBN = {978-3-642-02657-7},
DOI = {10.1007/978-3-642-02658-4_29},
}


Entry last modified by Anja Becker, 03/25/2010
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
03/24/2009 08:42:10 AM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Anja Becker
Swen Jacobs
Swen Jacobs
Swen Jacobs
Swen Jacobs
Edit Dates
25.03.2010 11:54:44
03/16/2010 10:43:54 AM
03/16/2010 10:41:46 AM
04/29/2009 03:31:27 PM
04/02/2009 04:10:52 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
IIGLR.pdf