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
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"
}
Back to top