Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30: Symbolic analysis and invariant synthesisVMCAI at Amphitheater 44
Chair(s): Constantin EneaLIAFA, Université Paris Diderot
16:00 - 16:30
Block-wise abstract interpretation by combining abstract domains with SMT
16:30 - 17:00
IC3 - Flipping the E in ICE
Yakir Vizel, Arie GurfinkelUniversity of Waterloo, Sharon ShohamTel Aviv university, Sharad MalikPrinceton University
17:00 - 17:30
Counterexample Validation and Interpolation-Based Refinement for Forest Automata
Lukáš Holík, Martin HruskaBrno University of Technology , Ondřej LengálBrno University of Technology , Adam RogalewiczBrno University of Technology , Tomáš VojnarBrno University of Technology