Publication Details

Programs with Lists are Counter Automata

IOSIF, R.; HABERMEHL, P.; VOJNAR, T.; BOUAJJANI, A.; BOZGA, M.; MORO, P. Programs with Lists are Counter Automata. In Computer Aided Verification. LNCS 4144. Berlin: Springer Verlag, 2006. p. 517-531. ISBN: 978-3-540-37406-0.

Czech title

Programy nad seznamy jsou čítačové automaty

Type

conference paper

Language

English

Authors

Radu Iosif
Habermehl Peter
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Bouajjani Ahmed
Bozga Marius
Moro Pierre

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

LNCS 4144

ISBN

978-3-540-37406-0

Publisher

Springer Verlag

Place

Berlin

BibTeX

@inproceedings{BUT34272,
  author="Iosif {Radu} and Peter {Habermehl} and Tomáš {Vojnar} and Ahmed {Bouajjani} and Marius {Bozga} and Pierre {Moro}",
  title="Programs with Lists are Counter Automata",
  booktitle="Computer Aided Verification",
  year="2006",
  series="LNCS 4144",
  pages="517--531",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-37406-0"
}