Result Details

Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. Static Analysis. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2006. p. 52-70. ISBN: 978-3-540-37756-6.
Type
conference paper
Language
English
Authors
Bouajjani Ahmed
Habermehl Peter
Rogalewicz Adam, doc. Mgr., Ph.D., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abstract

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.

Keywords

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

URL
Published
2006
Pages
52–70
Proceedings
Static Analysis
Series
Lecture Notes in Computer Science
Volume
4134
Conference
13th International Static Analysis Symposium -- SAS 2006
ISBN
978-3-540-37756-6
Publisher
Springer Verlag
Place
Berlin
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"
}
Projects
Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems, GACR, Postdoktorandské granty, GP102/03/D211, start: 2003-09-01, end: 2006-09-01, completed
Automated methods and tools supporting development of reliable parallel and distributed systems, GACR, Standardní projekty, GA102/04/0780, start: 2004-01-01, end: 2006-12-31, completed
Integrated approach to education of PhD students in the area of parallel and distributed systems, GACR, Doktorské granty, GD102/05/H050, start: 2005-01-01, end: 2008-12-31, completed
Research groups
Departments
Back to top