Detail publikace

Forester: From Heap Shapes to Automata Predicates

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

Originální název

Forester: From Heap Shapes to Automata Predicates

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Vydáno

7. 4. 2017

Nakladatel

Springer Verlag

Místo

Heidelberg

ISBN

978-3-662-54580-5

Kniha

Proceedings of TACAS'17

Edice

Lecture Notes in Computer Science

Strany od

365

Strany do

369

Strany počet

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

Dokumenty

06-HHLRSV-TACAS17.pdf