Detail výsledku

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

HRUŠKA, M.; HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. Brno: Faculty of Information Technology BUT, 2017. p. 1-23.
Typ
zpráva odborná
Jazyk
anglicky
Autoři
Hruška Martin, Ing., Ph.D., UITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., UITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Rogalewicz Adam, doc. Mgr., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
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.
http://www.fit.vutbr.cz/~lengal/pub/FIT-TR-2016-03.pdf

Klíčová slova

program analysis, shape analysis, counterexample validation, abstraction refinement, forest automata, tree automata

Rok
2017
Strany
1–23
Vydavatel
Faculty of Information Technology BUT
Místo
Brno
BibTeX 
@misc{BUT170108,
  author="Martin {Hruška} and Lukáš {Holík} and Ondřej {Lengál} and Adam {Rogalewicz} and Tomáš {Vojnar}",
  title="Counterexample Validation and Interpolation-Based Refinement for Forest Automata",
  year="2017",
  pages="1--23",
  publisher="Faculty of Information Technology BUT",
  address="Brno"
}
Pracoviště
Fakulta informačních technologií (FIT)
Nahoru