Publication Details

Programs with Lists are Counter Automata

BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre and VOJNAR Tomáš. Programs with Lists are Counter Automata. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 4144. Berlin: Springer Verlag, 2006, pp. 517-531. ISBN 978-3-540-37406-0.
Czech title
Programy nad seznamy jsou čítačové automaty
Type
conference paper
Language
english
Authors
Bouajjani Ahmed (UPAR7)
Bozga Marius (VERIMAG)
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Moro Pierre (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords

formal verification, model checking, programs with linked lists, counter automata, bisimulation

Abstract

We address the verification problem of programs manipulating one-selector linked data structures. We propose a new automated approach for checking safety and termination for these programs. Our approach is based on using counter automata as accurate abstract models: control states correspond to abstract heap graphs where list segments without sharing are collapsed, and counters are used to keep track of the number of elements in these segments. This allows to apply automatic analysis techniques and tools for counter automata in order to verify list programs. We show the effectiveness of our approach, in particular by verifying automatically termination of some sorting programs.

Published
2006
Pages
517-531
Proceedings
Computer Aided Verification
Series
Lecture Notes in Computer Science
Volume
4144
Conference
The 2006 Federated Logic Conference -- FLoC'06 / 18th International Conference on Computer-Aided Verification -- CAV'06, Seattle, Washington, US
ISBN
978-3-540-37406-0
Publisher
Springer Verlag
Place
Berlin, DE
BibTeX 
@INPROCEEDINGS{FITPUB8543,
   author = "Ahmed Bouajjani and Marius Bozga and Peter Habermehl and Radu Iosif and Pierre Moro and Tom\'{a}\v{s} Vojnar",
   title = "Programs with Lists are Counter Automata",
   pages = "517--531",
   booktitle = "Computer Aided Verification",
   series = "Lecture Notes in Computer Science",
   volume = 4144,
   year = 2006,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-37406-0",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8543"
}
Back to top