Jan 20, 2015: Tom van Dijk: IC3: Incremental Induction; SAT-based Model Checking Without Unrolling

January 20, 2015IC3: Incremental Induction; SAT-based Model Checking Without Unrolling
Room: HalB 2FTom van Dijk

In recent years a trending topic in Model Checking is using sophisticated techniques based around SAT checkers. These tools take a Boolean satisfiability problem, typically formulated as a set of clauses, and either return a satisfying assignment or a proof of unsatisfiability. This allows model checking without creating BDD representations of states and transitions, thus allowing checking much larger systems than in BDD-based symbolic model checking. A famous example is Bounded Model Checking, based around unrolling the transition relation for a bounded number of steps. While this method is great for finding bugs in a limited number of steps, it is much harder to prove correctness of a system, i.e., the inductive strengthening of some property. A new approach that is effective in proving the correctness of systems is called IC3. IC3 is based on incrementally refining abstractions of the state space based on counterexamples to induction and it is this topic that will be presented and discussed during the lunch lecture.