Deutsch
 
Benutzerhandbuch Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  On verifying complex properties using symbolic shape analysis

Wies, T., Kuncak, V., Zee, K., Podelski, A., & Rinard, M.(2006). On verifying complex properties using symbolic shape analysis (MPI-I-2006-2-001). Saarbrücken: Max-Planck-Institut für Informatik.

Item is

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: http://hdl.handle.net/11858/00-001M-0000-0014-6817-4 Versions-Permalink: http://hdl.handle.net/11858/00-001M-0000-0014-77BA-0
Genre: Bericht

Dateien

einblenden: Dateien
ausblenden: Dateien
:
MPI-I-2006-2-001.ps (beliebiger Volltext), 378KB
Name:
MPI-I-2006-2-001.ps
Beschreibung:
-
Sichtbarkeit:
Öffentlich
MIME-Typ / Prüfsumme:
application/postscript / [MD5]
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Wies, Thomas1, Autor              
Kuncak, Viktor2, Autor
Zee, Karen2, Autor
Podelski, Andreas1, Autor              
Rinard, Martin2, Autor
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
2External Organizations, ou_persistent22              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation such as linked data structures and arrays. We describe Bohne a new analysis for verifying data structures. Bohne verifies data structure operations and shows that 1) the operations preserve data structure invariants and 2) the operations satisfy their specifications expressed in terms of changes to the set of objects stored in the data structure. During the analysis Bohne infers loop invariants in the form of disjunctions of universally quantified Boolean combinations of formulas represented as sets of binary decision diagrams. To synthesize loop invariants of this form Bohne uses a combination of decision procedures for Monadic Second-Order Logic over trees SMT-LIB decision procedures (currently CVC Lite) and an automated reasoner within the Isabelle interactive theorem prover. This architecture shows that synthesized loop invariants can serve as a useful communication mechanism between different decision procedures. In addition Bohne uses field constraint analysis a combination mechanism that enables the use of uninterpreted function symbols within formulas of Monadic Second-Order Logic over trees. Using Bohne we have verified operations on data structures such as linked lists with iterators and back pointers trees with and without parent pointers two-level skip lists array data structures and sorted lists. We have deployed Bohne in the Hob and Jahob data structure analysis systems enabling us to combine Bohne with analyses of data structure clients and apply it in the context of larger programs. This report describes the Bohne algorithm as well as techniques that Bohne uses to reduce the ammount of annotations and the running time of the analysis.

Details

einblenden:
ausblenden:
Sprache(n): eng - Englisch
 Datum: 2006
 Publikationsstatus: Im Druck publiziert
 Seiten: 32 p.
 Ort, Verlag, Ausgabe: Saarbrücken : Max-Planck-Institut für Informatik
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: URI: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2006-2-001
Reportnr.: MPI-I-2006-2-001
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Research Report / Max-Planck-Institut für Informatik
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: - Identifikator: -