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.
Cite
CITATION STYLE
Holík, L., Hruška, M., Lengál, O., Rogalewicz, A., & Vojnar, T. (2017). Counterexample validation and interpolation-based refinement for forest automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10145 LNCS, pp. 288–309). Springer Verlag. https://doi.org/10.1007/978-3-319-52234-0_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
