Detail výsledku

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

HOLÍK, L.; HRUŠKA, M.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In Proceedings of VMCAI'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Cham: Springer Verlag, 2017. p. 288-309. ISBN: 978-3-319-52234-0. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D., UITS (FIT)
Hruška Martin, Ing., 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.

Klíčová slova


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

URL
Rok
2017
Strany
288–309
Časopis
Lecture Notes in Computer Science, roč. 10145, ISSN 0302-9743
Sborník
Proceedings of VMCAI'17
Řada
Lecture Notes in Computer Science
Konference
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)/Symposium on Principles of Programming Languages (POPL 2017)
ISBN
978-3-319-52234-0
Vydavatel
Springer Verlag
Místo
Cham
DOI
10.1007/978-3-319-52234-0_16
UT WoS
000413069800016
EID Scopus
2-s2.0-85010702893
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"
}
Soubory
Projekty
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Efektivní automaty pro formální rozhodování, GAČR, Juniorské granty, GJ16-24707Y, zahájení: 2016-01-01, ukončení: 2018-12-31, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru