de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Bounded model checking of pointer programs

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44970

Maier,  Patrick
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44232

Charatonik,  Witold
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44487

Georgieva,  Lilia
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

Charatonik_Georgieva_Maier_CSL2005_XT.ps
(beliebiger Volltext), 496KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Maier, P., Charatonik, W., & Georgieva, L.(2005). Bounded model checking of pointer programs (MPI-I-2005-2-002). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-6845-B
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.