Detail publikace

Programs with Lists are Counter Automata

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

Originální název

Programs with Lists are Counter Automata

Anglický název

Programs with Lists are Counter Automata

Jazyk

en

Originální abstrakt

We address the problem of verifying programs manipulating one-selector linked data structures. We propose and study in detail an application of counter automata as an accurate abstract model for this problem. We let control states of the counter automata correspond to abstract heap graphs where list segments without sharing are collapsed, and use counters to keep track of the number of elements in these segments. As a significant theoretical result, we show that the obtained counter automata are bisimilar to the original programs. Moreover, from a practical point of view, our translation allows one to apply efficient automatic analysis techniques and tools developed for counter automata (integer programs) in order to verify both safety as well as termination of list-manipulating programs. As another theoretical contribution, we prove that if the control of the generated counter automata does not contain nested loops (i.e., these automata are flat), both safety and termination are decidable for the original programs. Subsequently, we generalise our counter-automata-based model to keep track of ordering properties over lists storing ordered data. Finally, we show effectiveness of our approach by verifying automatically safety as well as termination of several sorting programs.

Anglický abstrakt

We address the problem of verifying programs manipulating one-selector linked data structures. We propose and study in detail an application of counter automata as an accurate abstract model for this problem. We let control states of the counter automata correspond to abstract heap graphs where list segments without sharing are collapsed, and use counters to keep track of the number of elements in these segments. As a significant theoretical result, we show that the obtained counter automata are bisimilar to the original programs. Moreover, from a practical point of view, our translation allows one to apply efficient automatic analysis techniques and tools developed for counter automata (integer programs) in order to verify both safety as well as termination of list-manipulating programs. As another theoretical contribution, we prove that if the control of the generated counter automata does not contain nested loops (i.e., these automata are flat), both safety and termination are decidable for the original programs. Subsequently, we generalise our counter-automata-based model to keep track of ordering properties over lists storing ordered data. Finally, we show effectiveness of our approach by verifying automatically safety as well as termination of several sorting programs.

Dokumenty

BibTex


@article{BUT76302,
  author="Tomáš {Vojnar} and Iosif {Radu} and Peter {Habermehl} and Ahmed {Bouajjani} and Marius {Bozga} and Pierre {Moro}",
  title="Programs with Lists are Counter Automata",
  annote="We address the problem of verifying programs manipulating one-selector linked
data structures. We propose and study in detail an application of counter
automata as an accurate abstract model for this problem. We let control states of
the counter automata correspond to abstract heap graphs where list segments
without sharing are collapsed, and use counters to keep track of the number of
elements in these segments. As a significant theoretical result, we show that the
obtained counter automata are bisimilar to the original programs. Moreover, from
a practical point of view, our translation allows one to apply efficient
automatic analysis techniques and tools developed for counter automata (integer
programs) in order to verify both safety as well as termination of
list-manipulating programs. As another theoretical contribution, we prove that if
the control of the generated counter automata does not contain nested loops
(i.e., these automata are flat), both safety and termination are decidable for
the original programs. Subsequently, we generalise our counter-automata-based
model to keep track of ordering properties over lists storing ordered data.
Finally, we show effectiveness of our approach by verifying automatically safety
as well as termination of several sorting programs.",
  address="NEUVEDEN",
  chapter="76302",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="2",
  volume="38",
  year="2011",
  month="april",
  pages="158--192",
  publisher="NEUVEDEN",
  type="journal article - other"
}