Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-2005-2-002

Bounded model checking of pointer programs

Maier, Patrick and Charatonik, Witold and Georgieva, Lilia

MPI-I-2005-2-002. May 2005, 34 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
Charatonik_Georgieva_Maier_CSL2005_XT.ps495 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2005-2-002
Hide details for BibTeXBibTeX
@TECHREPORT{MaierCharatonikGeorgieva2005,
  AUTHOR = {Maier, Patrick and Charatonik, Witold and Georgieva, Lilia},
  TITLE = {Bounded model checking of pointer programs},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2005-2-002},
  MONTH = {May},
  YEAR = {2005},
  ISSN = {0946-011X},
}