English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Incremental Instance Generation in Local Reasoning

Jacobs, S. (2009). Incremental Instance Generation in Local Reasoning. In A. Bouajjani, & O. Maler (Eds.), Computer Aided Verification (pp. 368-382). Berlin: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-1A5C-D Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-BBA0-E
Genre: Conference Paper

Files

show Files
hide Files
:
IIGLR.pdf (Any fulltext), 209KB
 
File Permalink:
-
Name:
IIGLR.pdf
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Jacobs, Swen1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2009-04-292009
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 521107
Other: Local-ID: C125716C0050FB51-F509A9DD2C874B41C1257583002A503E-Jacobs2009
DOI: 10.1007/978-3-642-02658-4_29
 Degree: -

Event

show
hide
Title: CAV 2009
Place of Event: Grenoble, France
Start-/End Date: 2009-06-29 - 2009-07-02

Legal Case

show

Project information

show

Source 1

show
hide
Title: Computer Aided Verification
  Abbreviation : CAV 2009
  Subtitle : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings
Source Genre: Proceedings
 Creator(s):
Bouajjani, Ahmed, Editor
Maler, Oded, Editor
Affiliations:
-
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 368 - 382 Identifier: -

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 5643 Sequence Number: - Start / End Page: - Identifier: -