Publication detail

Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

BOUAJJANI, A. HABERMEHL, P. ROGALEWICZ, A. VOJNAR, T.

Original Title

Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

Type

article in a collection out of WoS and Scopus

Language

English

Original Abstract

We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case studies.

Keywords

Formal verification, symbolic verification, shape analysis, dynamic data structures, tree automata.

Authors

BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T.

RIV year

2006

Released

29. 8. 2006

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-540-37756-6

Book

Static Analysis

Edition

Lecture Notes in Computer Science

Pages from

52

Pages to

70

Pages count

18

URL

http://www.fit.vutbr.cz/~rogalew/pubs/artmc_pointers.FULL.pdf

BibTex

@inproceedings{BUT30748,
  author="Ahmed {Bouajjani} and Peter {Habermehl} and Adam {Rogalewicz} and Tomáš {Vojnar}",
  title="Abstract Regular Tree Model Checking of Complex Dynamic Data Structures",
  booktitle="Static Analysis",
  year="2006",
  series="Lecture Notes in Computer Science",
  volume="4134",
  pages="52--70",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-37756-6",
  url="http://www.fit.vutbr.cz/~rogalew/pubs/artmc_pointers.FULL.pdf"
}