Publication detail

Forester: From Heap Shapes to Automata Predicates

HRUŠKA, M. HOLÍK, L. LENGÁL, O. ROGALEWICZ, A. ŠIMÁČEK, J. VOJNAR, T.

Original Title

Forester: From Heap Shapes to Automata Predicates

Type

conference paper

Language

English

Original 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.

Keywords

program verification
forest automata
shape analysis
memory safety
heap manipulation
dynamic data structures
backward run
abstraction refinement

Authors

HRUŠKA, M.; HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.

Released

7. 4. 2017

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-662-54580-5

Book

Proceedings of TACAS'17

Edition

Lecture Notes in Computer Science

Pages from

365

Pages to

369

Pages count

4

URL

https://www.fit.vut.cz/research/publication/11414/

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/"
}

Documents

06-HHLRSV-TACAS17.pdf