Detail publikace

Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; MORO, P. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2005. p. 13-29. ISBN: 978-3-540-25333-4.
Název česky
Verifikace programů s dynamickými datovými strukturami s jedním ukazatelem na následníka pomocí regulárního model checkingu
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Bouajjani Ahmed
Habermehl Peter
Moro Pierre
URL
Klíčová slova

formální verifikace, model checking, nekonečně stavové systémy, verifikace software, dynamické datové struktury

Abstrakt

Článek navrhuje originální metodu verifikace programů s neomezenýmidynamickými datovými strutkurami s jedním ukazatelem na následníka(seznamy, cyklické seznamy) pomocí regulárního mode checkingu. Jenavržen konečný způsob reprezentace nekonečných množin stavů programůs uvedenými datovými strukturami pomocí konečných automatů. Příkazymanipulující s těmito strukturami jsou modelovány pomocí konečnýchpřevodníků. Opakovanou aplikací převodníků na počáteční množinu stavůse pak počítá množina všech dosažitelných stavů, přičemž pro zajištěníkonečnosti výpočtu v co největším počtu případů jsou použityoriginální metody abstrakce nad automaty (obecně konečnost zajistit nelze, neboť daný verifikační problém je nerozhodnutelný).

Rok
2005
Strany
13–29
Sborník
Tools and Algorithms for the Construction and Analysis of Systems
Řada
Lecture Notes in Computer Science
Svazek
3440
Konference
11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems -- TACAS 2005, Edinburgh, GB
ISBN
978-3-540-25333-4
Vydavatel
Springer Verlag
Místo
Berlin
BibTeX 
@inproceedings{BUT32780,
  author="Tomáš {Vojnar} and Ahmed {Bouajjani} and Peter {Habermehl} and Pierre {Moro}",
  title="Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2005",
  series="Lecture Notes in Computer Science",
  volume="3440",
  pages="13--29",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-25333-4",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/bhmv-lists-05.ps.gz"
}
Nahoru