Detail publikace

Fully Automated Shape Analysis Based on Forest Automata

HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. Proceedings of CAV'13. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2013. p. 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
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Lengál Ondřej, Ing., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Klíčová slova

forest automata, shape analysis, dynamic linked data structures, tree automata, abstraction

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
ISBN
978-3-642-39798-1
Vydavatel
Springer Verlag
Místo
Heidelberg
BibTeX 
@inproceedings{BUT103488,
  author="Lukáš {Holík} and Ondřej {Lengál} and Adam {Rogalewicz} and Jiří {Šimáček} and Tomáš {Vojnar}",
  title="Fully Automated Shape Analysis Based on Forest Automata",
  booktitle="Proceedings of CAV'13",
  year="2013",
  journal="Lecture Notes in Computer Science",
  number="8044",
  pages="740--755",
  publisher="Springer Verlag",
  address="Heidelberg",
  isbn="978-3-642-39798-1",
  issn="0302-9743"
}
Nahoru