Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Charatonik, Witold
Georgieva, Lilia
Maier, Patrick

dblp
dblp
dblp

Not MPG Author(s):

Charatonik, Witold
Georgieva, Lilia

Editor(s):

Ong, Luke

dblp

Not MPII Editor(s):

Ong, Luke

BibTeX cite key*:

CharatonikGeorgievaMaier2005

Title, Booktitle

Title*:

Bounded Model Checking of Pointer Programs

Booktitle*:

Computer Science Logic; 19th International Workshop, CSL 2005; 14th Annual Conference of the EACSL

Event, URLs

URL of the conference:

http://web.comlab.ox.ac.uk/oucl/conferences/CSL05/

URL for downloading the paper:


Event Address*:

Oxford, UK

Language:

English

Event Date*
(no longer used):


Organization:

European Association for Computer Science Logic (EACSL)

Event Start Date:

22 August 2005

Event End Date:

25 August 2005

Publisher

Name*:

Springer

URL:

http://www.springer.com

Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

3634

Number:


Month:

August

Pages:

397-412

Year*:

2005

VG Wort Pages:


ISBN/ISSN:

3-540-28231-9

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) 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.

Keywords:

decidable fragments, pointer verification, model checking

Copyright Message:

Copyright Springer-Verlag Berlin Heidelberg 2005


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort



BibTeX Entry:

@INPROCEEDINGS{CharatonikGeorgievaMaier2005,
AUTHOR = {Charatonik, Witold and Georgieva, Lilia and Maier, Patrick},
EDITOR = {Ong, Luke},
TITLE = {Bounded Model Checking of Pointer Programs},
BOOKTITLE = {Computer Science Logic; 19th International Workshop, CSL 2005; 14th Annual Conference of the EACSL},
PUBLISHER = {Springer},
YEAR = {2005},
ORGANIZATION = {European Association for Computer Science Logic (EACSL)},
VOLUME = {3634},
PAGES = {397--412},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Oxford, UK},
MONTH = {August},
ISBN = {3-540-28231-9},
}


Entry last modified by Christine Kiesel, 01/28/2008
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Patrick Maier
Created
11/10/2005 07:32:09 PM
Revision
1.
0.


Editor
Christine Kiesel
Patrick Maier


Edit Date
21.12.2005 10:08:59
11/10/2005 07:32:09 PM


Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section