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. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013. p. 1-25.
Název česky
Plně automatizovaná analýza haldy programů založená na lesních automatech
Typ
zpráva odborná
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)
URL
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
1–25
Vydavatel
Faculty of Information Technology BUT
Místo
FIT-TR-2013-01, Brno
BibTeX 
@techreport{BUT192914,
  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",
  year="2013",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2013-01, Brno",
  pages="1--25",
  url="http://www.fit.vutbr.cz/~ilengal/pub/FIT-TR-2013-01.pdf"
}
Nahoru