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. In Tools and Algorithms for the Construction and Analysis of Systems. LNCS 3440. 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ými dynamickými datovými strutkurami s jedním ukazatelem na následníka (seznamy, cyklické seznamy) pomocí regulárního mode checkingu. Je navrž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říkazy manipulující s těmito strukturami jsou modelovány pomocí konečných př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žity originá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
LNCS 3440
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="LNCS 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