Counterexample Validation and Interpolation-Based Refinement for Forest Automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU122837" target="_blank" >RIV/00216305:26230/17:PU122837 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007/978-3-319-52234-0_16" target="_blank" >http://link.springer.com/chapter/10.1007/978-3-319-52234-0_16</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-52234-0_16" target="_blank" >10.1007/978-3-319-52234-0_16</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of VMCAI'17

ISBN

978-3-319-52234-0

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

22

Strana od-do

288-309

Název nakladatele

Springer Verlag

Místo vydání

Cham

Místo konání akce

Paříž

Datum konání akce

15. 1. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000413069800016