Publication Details
Forester: From Heap Shapes to Automata Predicates
HRUŠKA Martin, HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forester: From Heap Shapes to Automata Predicates. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10206. Heidelberg: Springer Verlag, 2017, pp. 365-369. ISBN 978-3-662-54580-5.
Czech title
Lesník: Od tvarů hromady k automatovým predikátům
Type
conference paper
Language
english
Authors
Hruška Martin, Ing. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Šimáček Jiří, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Šimáček Jiří, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords
program verification
forest automata
shape analysis
memory safety
heap manipulation
dynamic data structures
backward run
abstraction refinement
Abstract
This paper describes the participation of Forester in the SV-COMP 2017 competition on software verification. We briefly present the verification procedure used by Forester, the architecture of Forester, and changes in Forester done since the previous year of SV-COMP, in particular the fully-automatically refinable abstraction for hierarchical
forest automata.
Published
2017
Pages
365-369
Proceedings
Proceedings of TACAS'17
Series
Lecture Notes in Computer Science
Volume
10206
Conference
European Joint Conferences on Theory and Practice of Software, Uppsala, SE
ISBN
978-3-662-54580-5
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
UT WoS
000440733400024
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11414, author = "Martin Hru\v{s}ka and 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 = "Forester: From Heap Shapes to Automata Predicates", pages = "365--369", booktitle = "Proceedings of TACAS'17", series = "Lecture Notes in Computer Science", volume = 10206, year = 2017, location = "Heidelberg, DE", publisher = "Springer Verlag", ISBN = "978-3-662-54580-5", doi = "10.1007/978-3-662-54580-5\_24", language = "english", url = "https://www.fit.vut.cz/research/publication/11414" }