Detail publikace

Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

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

Originální název

Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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

Klíčová slova

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

Autoři

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

Rok RIV

2006

Vydáno

29. 8. 2006

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-540-37756-6

Kniha

Static Analysis

Edice

Lecture Notes in Computer Science

Strany od

52

Strany do

70

Strany počet

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"
}