Publication result 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

English Title

Forester: From Heap Shapes to Automata Predicates

Type

Paper in proceedings (conference paper)

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.

English 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

Key words in English

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.

RIV year

2018

Released

07.04.2017

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-662-54580-5

Book

Proceedings of TACAS'17

Edition

Lecture Notes in Computer Science

Volume

10206

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