Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HOLÍK, L. HRUŠKA, M. LENGÁL, O. ROGALEWICZ, A. VOJNAR, T.
Originální název
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
In the context of shape analysis, counterexample validation and abstraction refinement are complex and so far not sufficiently resolved problems. We provide a novel solution to both of these problems in the context of fully automated and rather general shape analysis based on forest automata. Our approach is based on backward symbolic execution on forest automata, allowing one to derive automata-based interpolants and refine the automata abstraction used. The approach allows one to distinguish true and spurious counterexamples and guarantees progress of the abstraction refinement. We have implemented the approach in the FORESTER tool and present promising experimental results.
Klíčová slova
program analysis, shape analysis, counterexample validation, abstraction refinement, forest automata, tree automata
Autoři
HOLÍK, L.; HRUŠKA, M.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T.
Vydáno
17. 1. 2017
Nakladatel
Springer Verlag
Místo
Cham
ISBN
978-3-319-52234-0
Kniha
Proceedings of VMCAI'17
Edice
Lecture Notes in Computer Science
ISSN
0302-9743
Periodikum
Ročník
10145
Stát
Spolková republika Německo
Strany od
288
Strany do
309
Strany počet
22
URL
http://link.springer.com/chapter/10.1007/978-3-319-52234-0_16
BibTex
@inproceedings{BUT133502, author="Lukáš {Holík} and Martin {Hruška} and Ondřej {Lengál} and Adam {Rogalewicz} and Tomáš {Vojnar}", title="Counterexample Validation and Interpolation-Based Refinement for Forest Automata", booktitle="Proceedings of VMCAI'17", year="2017", series="Lecture Notes in Computer Science", journal="Lecture Notes in Computer Science", volume="10145", pages="288--309", publisher="Springer Verlag", address="Cham", doi="10.1007/978-3-319-52234-0\{_}16", isbn="978-3-319-52234-0", issn="0302-9743", url="http://link.springer.com/chapter/10.1007/978-3-319-52234-0_16" }