Detail publikace

Fully Automated Shape Analysis Based on Forest Automata

HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, s. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.
Název česky
Plně automatizovaná analýza haldy programů založená na lesních automatech
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Abstrakt

Lesní automaty byly v nedávné době navrženy jako nástroj pro analýzu komplexních struktur v haldách programů. Lesní automaty reprezentují množinu stromových dekompozicí grafů haldy ve formě uspořádané množiny stromových automatů. S ohledem na možnost reprezentace složitých datových struktur na haldě umožňoval formalismus lesních automatů uživateli dodat sadu lesních automatů (nazývaných krabice), které reprezentovaly opakující se vzory v grafu haldy, jako symboly jiných lesních automatů vyšší úrovně. V tomto článku navrhujeme inovativní techniku automatického učení se krabic, která umožňuje vyhnout se kroku jejich manuální konstrukce. Dále navrhujeme podstatné vylepšení automatové abstrakce použité v analýze. Výsledkem je efektivní, plně automatizovaná analýza která umožňuje verifikaci i tak složitých datových struktur, jako jsou například přeskakované seznamy. Výkon této analýzy je srovnatelný s nejmodernějšími plně automatizovanými nástroji založenými na separační logice, které jsou však specializované pouze na programy se seznamy.

Rok
2013
Strany
740-755
Časopis
Lecture Notes in Computer Science, č. 8044, ISSN 0302-9743
Sborník
Proceedings of CAV'13
Konference
25th International Conference on Computer Aided Verification -- CAV 2013, Saint Petersburg, RU
ISBN
978-3-642-39798-1
Vydavatel
Springer Verlag
Místo
Heidelberg, DE
BibTeX
@INPROCEEDINGS{FITPUB10322,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l and Adam Rogalewicz and Ji\v{r}\'{i} \v{S}im\'{a}\v{c}ek and Tom\'{a}\v{s} Vojnar",
   title = "Fully Automated Shape Analysis Based on Forest Automata",
   pages = "740--755",
   booktitle = "Proceedings of CAV'13",
   journal = "Lecture Notes in Computer Science",
   number = 8044,
   year = 2013,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-39798-1",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10322"
}
Nahoru