Publication Details

Counterexample Validation and Interpolation-Based Refinement for Forest Automata

HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam and VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Lecture Notes in Computer Science, vol. 10145. Cham: Springer Verlag, 2017, pp. 288-309. ISBN 978-3-319-52234-0. ISSN 0302-9743. Available from: http://link.springer.com/chapter/10.1007/978-3-319-52234-0_16
Czech title
Ověřování protipříkladů a zjemňovaní abstrakce založené na interpolantech pro lesní automaty
Type
conference paper
Language
english
Authors
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Hruška Martin, Ing. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords


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

Abstract

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.

Published
2017
Pages
288-309
Journal
Lecture Notes in Computer Science, vol. 10145, ISSN 0302-9743
Proceedings
Proceedings of VMCAI'17
Series
Lecture Notes in Computer Science
Conference
International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)/Symposium on Principles of Programming Languages (POPL 2017), Paříž, FR
ISBN
978-3-319-52234-0
Publisher
Springer Verlag
Place
Cham, DE
DOI
10.1007/978-3-319-52234-0_16
UT WoS
000413069800016
EID Scopus
2-s2.0-85010702893
BibTeX 
@INPROCEEDINGS{FITPUB11300,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Martin Hru\v{s}ka and Ond\v{r}ej Leng\'{a}l and Adam Rogalewicz and Tom\'{a}\v{s} Vojnar",
   title = "Counterexample Validation and Interpolation-Based Refinement for Forest Automata",
   pages = "288--309",
   booktitle = "Proceedings of VMCAI'17",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 10145,
   year = 2017,
   location = "Cham, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-319-52234-0",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-319-52234-0\_16",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11300"
}
Back to top