Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Bounded Model Checking of Pointer Programs

Charatonik, W., Georgieva, L., & Maier, P. (2005). Bounded Model Checking of Pointer Programs. In Computer Science Logic; 19th International Workshop, CSL 2005; 14th Annual Conference of the EACSL (pp. 397-412). Berlin, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-25FC-E Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-25FE-A
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Charatonik, Witold1, Autor           
Georgieva, Lilia1, Autor           
Maier, Patrick1, Autor           
Ong, Luke, Herausgeber
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We propose a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. Our procedure checks whether a program execution of length n ends in an error (e.g., a NULL dereference) by testing if the weakest precondition of the error condition together with the initial condition of the program (e.g., program variable x points to a circular list) is satisfiable. We express error conditions as formulas in the 2-variable fragment of the Bernays-Schoenfinkel class with equality. We show that this fragment is closed under computing weakest preconditions. We express the initial conditions by unary relations which are defined by monadic Datalog programs. Our main contribution is a small model theorem for the 2-variable fragment of the Bernays-Schoenfinkel class extended with least fixed points expressible by certain monadic Datalog programs. The decidability of this extension of first-order logic gives us a bounded model checking procedure for programs manipulating dynamically allocated pointer structures. In contrast to SAT-based bounded model checking, we do not bound the size of the heap a priori, but allow for pointer structures of arbitrary size. Thus, we are doing bounded model checking of infinite state transition systems.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2005-12-212005
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 279105
Anderer: Local-ID: C1256104005ECAFC-B84D6259621B6394C12570B50065D231-CharatonikGeorgievaMaier2005
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Oxford, UK
Start-/Enddatum: 2005-08-22

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Computer Science Logic; 19th International Workshop, CSL 2005; 14th Annual Conference of the EACSL
Genre der Quelle: Konferenzband
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 397 - 412 Identifikator: ISBN: 3-540-28231-9

Quelle 2

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