Conference paper

BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Static Analysis. Berlin: Springer Verlag, 2006, pp. 52-70. ISBN 978-3-540-37756-6.
Publication language:english
Original title:Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
Title (cs):Verifikace komplexních dynamických datových struktur za použitím abstraktního regulárního stromového model checkingu
Proceedings:Static Analysis
Conference:13th International Static Analysis Symposium -- SAS 2006
Series:LNCS 4134
Place:Berlin, DE
Publisher:Springer Verlag
Formal verification, symbolic verification, shape analysis, dynamic data structures, tree automata.
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.
   author = {Ahmed Bouajjani and Peter Habermehl and Adam
	Rogalewicz and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Abstract Regular Tree Model Checking of Complex
	Dynamic Data Structures},
   pages = {52--70},
   booktitle = {Static Analysis},
   series = {LNCS 4134},
   year = 2006,
   location = {Berlin, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-540-37756-6},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https