Detail publikace

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

BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre a VOJNAR Tomáš. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 3440. Berlin: Springer Verlag, 2005, s. 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
angličtina
Autoři
Bouajjani Ahmed (UPAR7)
Habermehl Peter (UPAR7)
Moro Pierre (LIAFA UP7/CNRS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
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
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, DE
BibTeX 
@INPROCEEDINGS{FITPUB7814,
   author = "Ahmed Bouajjani and Peter Habermehl and Pierre Moro and Tom\'{a}\v{s} Vojnar",
   title = "Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking",
   pages = "13--29",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Lecture Notes in Computer Science",
   volume = 3440,
   year = 2005,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-25333-4",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7814"
}
Nahoru