Technical Report PHD-2014-09

Title: SAT-based Model Checking Using Interpolation and IC3
Authors: Yakir Vizel
Supervisors: Professor Orna Grumberg
Abstract: SAT-based model checking is currently one of the most successful approaches to checking very large systems. In its early days, SAT-based (bounded) model checking was mainly used for bug hunting. The introduction of interpolation and IC3/PDR enable efficient complete algorithms that can provide full verification as well.

In this thesis, we preset several approaches to enhancing SAT-based model checking. They are all based on iteratively computing an over-approximation of the set of reachable system states. They use different mechanisms to achieve scalability and faster convergence (empirically). 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 using the structure of the model checking problem and applying inductive reasoning. This results in an efficient procedure that generates compact interpolants in Conjunctive Normal Form.

The last approach we present integrates lazy abstraction with IC3 in order to achieve scalability. Lazy abstraction, originally developed for software model checking, is a specific type of abstraction that allows hiding different model details at different steps of the verification. We find the IC3 algorithm most suitable for lazy abstraction since its state traversal is performed by means of local reachability checks, each involving only two consecutive sets. A different abstraction can therefore be applied in each of the local checks. The techniques presented in this thesis make SAT-based model checking more scalable. The thesis focuses on hardware model checking, but the presented ideas can be extended to other systems as well.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the PHD technical reports of 2014
To the main CS technical reports page

Computer science department, Technion