Detail publikace

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

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

Lecture Notes in Computer Science

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