Bounded model checking of pointer programs

Witold Charatonik, Lilia Georgieva, Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

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-Schönfinkel 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-Schönfinkel 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.

Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005. Proceedings
EditorsLuke Ong
Pages397-412
Number of pages16
Volume3634
ISBN (Electronic)978-3-540-31897-2
DOIs
Publication statusPublished - Aug 2005
Event19th International Workshop on Computer Science Logic ,and 14th Annual Conference of the EACSL - Oxford, United Kingdom
Duration: 22 Aug 200525 Aug 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3634
ISSN (Print)0302-9743

Conference

Conference19th International Workshop on Computer Science Logic ,and 14th Annual Conference of the EACSL
Abbreviated titleCSL 2005
CountryUnited Kingdom
CityOxford
Period22/08/0525/08/05

Keywords

  • decidable fragments
  • pointer verification
  • model checking

Fingerprint Dive into the research topics of 'Bounded model checking of pointer programs'. Together they form a unique fingerprint.

Cite this