POPL 2017 (series) / VMCAI 2017 (series) / VMCAI /
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Mon 16 Jan 2017 17:00 - 17:30 at Amphitheater 44 - Symbolic analysis and invariant synthesis Chair(s): Constantin Enea
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 (nested) 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
Mon 16 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 16 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44 Chair(s): Constantin Enea LIAFA, Université Paris Diderot | ||
16:00 30mTalk | Block-wise abstract interpretation by combining abstract domains with SMT VMCAI | ||
16:30 30mTalk | IC3 - Flipping the E in ICE VMCAI Yakir Vizel , Arie Gurfinkel University of Waterloo, Sharon Shoham Tel Aviv university, Sharad Malik Princeton University | ||
17:00 30mTalk | Counterexample Validation and Interpolation-Based Refinement for Forest Automata VMCAI Lukáš Holík , Martin Hruska Brno University of Technology , Ondřej Lengál Brno University of Technology , Adam Rogalewicz Brno University of Technology , Tomáš Vojnar Brno University of Technology | ||