Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  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

Dateien

einblenden: Dateien
ausblenden: Dateien
:
IIGLR.pdf (beliebiger Volltext), 209KB
 
Datei-Permalink:
-
Name:
IIGLR.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/pdf
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Jacobs, Swen1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2009-04-292009
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 521107
Anderer: Local-ID: C125716C0050FB51-F509A9DD2C874B41C1257583002A503E-Jacobs2009
DOI: 10.1007/978-3-642-02658-4_29
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: CAV 2009
Veranstaltungsort: Grenoble, France
Start-/Enddatum: 2009-06-29 - 2009-07-02

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Computer Aided Verification
  Kurztitel : CAV 2009
  Untertitel : 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings
Genre der Quelle: Konferenzband
 Urheber:
Bouajjani, Ahmed, Herausgeber
Maler, Oded, Herausgeber
Affiliations:
-
Ort, Verlag, Ausgabe: Berlin : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 368 - 382 Identifikator: -

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
  Kurztitel : LNCS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 5643 Artikelnummer: - Start- / Endseite: - Identifikator: -