Detail publikace

Programs with Lists are Counter Automata

VOJNAR, T.; IOSIF, R.; HABERMEHL, P.; BOUAJJANI, A.; BOZGA, M.; MORO, P. Programs with Lists are Counter Automata. FORMAL METHODS IN SYSTEM DESIGN, 2011, vol. 38, no. 2, p. 158-192. ISSN: 0925-9856.
Název česky
Programy nad seznamy odpovídají automatům s čítači
Typ
článek v časopise
Jazyk
anglicky
Autoři
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Radu Iosif
Habermehl Peter
Bouajjani Ahmed
Bozga Marius
Moro Pierre
URL
Klíčová slova

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

Abstrakt

Článek dokazuje, že programy nad jednosměrně vázanými seznamy jsou bisimilární s čítačovými automaty. Uvedený výsledek se dá využít k verifikaci jak bezpečnosti tak konečnosti běhu takových programů. Článek dále ukazuje, že programy nad seznamy s daty, nad kterými je definována relace uspořádání, lze efektivně simulovat čítačovými automaty.

Rok
2011
Strany
158–192
Časopis
FORMAL METHODS IN SYSTEM DESIGN, roč. 38, č. 2, ISSN 0925-9856
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",
  journal="FORMAL METHODS IN SYSTEM DESIGN",
  year="2011",
  volume="38",
  number="2",
  pages="158--192",
  issn="0925-9856",
  url="http://www.springerlink.com/content/323xp67u84550134/"
}
Nahoru