Yakir Vizel

Date: 16:00, Tuesday, October 15, 2013
Speaker: Yakir Vizel
Venue: IST Austria

Model checking is an automatic approach to formally verifying that a given system satisfies a given specification. Nowadays, most state-of-the-art model checking algorithms are based on SAT (and SMT) solvers. In its early days, SAT-based model checking was mostly used for Bounded Model Checking (BMC) and therefore could only refute properties. The introduction of interpolation into model checking enabled an efficient, sound and complete SAT-based algorithm. This algorithm is usually referred to as interpolationbased model checking (ITP). While being efficient, a main drawback of the approach is the size of generated interpolants. When interpolants generated by ITP become extremely large, the procedure becomes slow or even intractable. In this talk, we introduce several methods that use interpolation, but try to overcome the problems imposed by the size of interpolants. The first approach uses interpolation-sequence, rather than interpolation, in order to obtain a more precise over-approximation of the set of reachable states and avoids the addition of interpolants into the BMC formula. The second approach extracts interpolants in both forward and backward manner and exploits them for an intertwined approximated forward and backward reachability analysis. The approach is also mostly local and avoids unrolling of the checked model as much as possible. By that, the size of interpolants is mostly kept small. This results in an efficient and complete SAT-based verification algorithm. The third approach takes a different direction. It suggests a new method for interpolant computation which is specific for model checking. As a first step, it approximates the interpolant using a proof generated by the SAT solver. The second step transforms the approximated interpolant into a real interpolant by applying inductive reasoning. This results in an efficient procedure that generates compact interpolants in Conjunctive Normal Form. We conclude with suggestions for future research
Posted in RiSE Seminar