Conference paper

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. Heidelberg: Springer Verlag, 2017, pp. 365-369. ISBN 978-3-662-54580-5.
Publication language:english
Original title:Forester: From Heap Shapes to Automata Predicates
Title (cs):Lesník: Od tvarů hromady k automatovým predikátům
Pages:365-369
Proceedings:Proceedings of TACAS'17
Conference:European Joint Conferences on Theory and Practice of Software -- ETAPS'17 (TACAS'17)
Series:LNCS 10206
Place:Heidelberg, DE
Year:2017
ISBN:978-3-662-54580-5
Publisher:Springer Verlag
Keywords
program verification
forest automata
shape analysis
memory safety
heap manipulation
dynamic data structures
backward run
abstraction refinement
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   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 = {LNCS 10206},
   year = {2017},
   location = {Heidelberg, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-662-54580-5},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en?id=11414}
}

Your IPv4 address: 54.163.210.170
Switch to IPv6 connection

DNSSEC [dnssec]