Publication Details

Forester: From Heap Shapes to Automata Predicates

HRUŠKA, M.; HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Forester: From Heap Shapes to Automata Predicates. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 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., Ph.D. (Automata@FIT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
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
ISBN
978-3-662-54580-5
Publisher
Springer Verlag
Place
Heidelberg
DOI
10.1007/978-3-662-54580-5_24
UT WoS
000440733400024
EID Scopus
2-s2.0-85017522557
BibTeX 
@inproceedings{BUT134718,
  author="Martin {Hruška} and Lukáš {Holík} and Ondřej {Lengál} and Adam {Rogalewicz} and Jiří {Šimáček} and Tomáš {Vojnar}",
  title="Forester: From Heap Shapes to Automata Predicates",
  booktitle="Proceedings of TACAS'17",
  year="2017",
  series="Lecture Notes in Computer Science",
  volume="10206",
  pages="365--369",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-662-54580-5\{_}24",
  isbn="978-3-662-54580-5",
  url="https://www.fit.vut.cz/research/publication/11414/"
}
Back to top