English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Bounded model checking of pointer programs

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.

Item is

Files

show Files
hide Files
:
Charatonik_Georgieva_Maier_CSL2005_XT.ps (Any fulltext), 496KB
Name:
Charatonik_Georgieva_Maier_CSL2005_XT.ps
Description:
-
OA-Status:
Visibility:
Public
MIME-Type / Checksum:
application/postscript / [MD5]
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Maier, Patrick1, Author           
Charatonik, Witold1, Author           
Georgieva, Lilia1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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-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

show
hide
Language(s): eng - English
 Dates: 2005
 Publication Status: Issued
 Pages: 34 p.
 Publishing info: Saarbrücken : Max-Planck-Institut für Informatik
 Table of Contents: -
 Rev. Type: -
 Identifiers: URI: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2005-2-002
Report Nr.: MPI-I-2005-2-002
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Research Report / Max-Planck-Institut für Informatik
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: - Identifier: -