SAT-Based Model Checking with Interpolation

This talk is a tutorial on interpolation in verification.

Model checking is an automatic approach to formally verify that a given system satisfies a given specification. SAT-based model checking is most efficient in finding bugs in large systems. When combined with interpolation, it can also provide full verification.

We describe the use of interpolation in SAT-based model checking and survey several approaches to enhance its power.

We will assume no previous knowledge on model checking or interpolation. All the needed background will be given.