Conference paper

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. Cham: Springer Verlag, 2017, pp. 288-309. ISBN 978-3-319-52234-0. Available from: http://link.springer.com/chapter/10.1007/978-3-319-52234-0_16
Publication language:english
Original title:Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Title (cs):Ověřování protipříkladů a zjemňovaní abstrakce založené na interpolantech pro lesní automaty
Pages:288-309
Proceedings:Proceedings of VMCAI'17
Conference:International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)/Symposium on Principles of Programming Languages (POPL 2017)
Series:Lecture Notes in Computer Science 10145
Place:Cham, DE
Year:2017
URL:http://link.springer.com/chapter/10.1007/978-3-319-52234-0_16
ISBN:978-3-319-52234-0
Publisher:Springer Verlag
Files: 
+Type Name Title Size Last modified
iconforester-refinement.pdf379 KB2017-03-08 14:07:12
^ Select all
With selected:
Keywords
program analysis, shape analysis, counterexample validation, abstraction refinement, forest automata, tree automata
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   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 10145},
   year = {2017},
   location = {Cham, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-319-52234-0},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11300}
}

Your IPv4 address: 54.80.137.168
Switch to IPv6 connection

DNSSEC [dnssec]