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

Induction is a key element of state-of-the-art verification techniques. Automatically synthesizing and verifying inductive invariants is at the heart of Model Checking of safety properties. In this paper, we study the relationship between two popular approaches to synthesizing inductive invariants: SAT-based Model Checking (SAT-MC) and Machine Learning-based Invariant Synthesis (MLIS). Our goal is to identify and formulate the theoretical similarities and differences between the two frameworks. We focus on two flagship algorithms: IC3 (an instance of SAT-MC) and ICE (an instance of MLIS). We show that the two frameworks are very similar yet distinct. For a meaningful comparison, we introduce RICE, an extension of ICE with relative induction and show how IC3 can be implemented as an instance of RICE. We believe this work contributes to the understanding of inductive invariant synthesis and will serve as a foundation for further improvements to both SAT-MC and MLIS algorithms.

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
30m
Talk
Block-wise abstract interpretation by combining abstract domains with SMT
VMCAI
16:30
30m
Talk
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
30m
Talk
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