Faculty of Information Technology, BUT

Publication Details

Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre and VOJNAR Tomáš. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3440. Berlin: Springer Verlag, 2005, pp. 13-29. ISBN 978-3-540-25333-4.
Czech title
Verifikace programů s dynamickými datovými strukturami s jedním ukazatelem na následníka pomocí regulárního model checkingu
Type
conference paper
Language
english
Authors
Bouajjani Ahmed (UPAR7)
Habermehl Peter (UPAR7)
Moro Pierre (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords
formal verification, model checking, infinite-state systems, software verification, dynamic data structures
Abstract
We address the problem of automatic verification of programs with dynamic data structures. We consider the case of sequential, non-recursive programs manipulating 1-selector-linked structures such as traditional linked lists (possibly sharing their tails) and circular lists. We propose an automata-based approach for a symbolic verification of such programs using the regular model checking framework. Given a program, the configurations of the memory are systematically encoded as words over a suitable finite alphabet, potentially infinite sets of configurations are represented by finite-state automata, and statements of the program are automatically translated into finite-state transducers defining regular relations between configurations. Then, abstract regular model checking techniques are applied in order to automatically check safety properties concerning the shape of the computed configurations or relating the input and output configurations. For this particular purpose, we introduce new techniques for the computation of abstractions of the set of reachable configurations and to refine these abstractions if spurious counterexamples are detected.  Finally, we present experimental results showing the applicability of the approach and its efficiency.

Published
2005
Pages
13-29
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Volume
3440
Conference
11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems -- TACAS 2005, Edinburgh, GB
ISBN
978-3-540-25333-4
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB7814,
   author = "Ahmed Bouajjani and Peter Habermehl and Pierre Moro and Tom\'{a}\v{s} Vojnar",
   title = "Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking",
   pages = "13--29",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Lecture Notes in Computer Science",
   volume = 3440,
   year = 2005,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-25333-4",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7814"
}
Back to top