Detail publikace

Programs with Lists are Counter Automata

IOSIF, R. HABERMEHL, P. VOJNAR, T. BOUAJJANI, A. BOZGA, M. MORO, P.

Originální název

Programs with Lists are Counter Automata

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

We address the verification problem of programs manipulatingone-selector linked data structures. We propose a new automatedapproach for checking safety and termination for these programs. Ourapproach is based on using counter automata as accurate abstractmodels: control states correspond to abstract heap graphs where listsegments without sharing are collapsed, and counters are used to keeptrack of the number of elements in these segments. This allows to applyautomatic analysis techniques and tools for counter automata in orderto verify list programs. We show the effectiveness of our approach, inparticular by verifying automatically termination of some sortingprograms.

Klíčová slova

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

Autoři

IOSIF, R.; HABERMEHL, P.; VOJNAR, T.; BOUAJJANI, A.; BOZGA, M.; MORO, P.

Rok RIV

2006

Vydáno

10. 7. 2006

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-540-37406-0

Kniha

Computer Aided Verification

Edice

Lecture Notes in Computer Science

Strany od

517

Strany do

531

Strany počet

15

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="Lecture Notes in Computer Science",
  volume="4144",
  pages="517--531",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-37406-0"
}