Model Checking with Boolean Satisfiability

Joao Marques Silva

(Southampton)

The evolution of SAT technology over the last decade has motivated its application to model checking, initially through the utilization of SAT in bounded model checking and, more recently, in unbounded model checking. Among the techniques proposed for unbounded model checking, the utilization of interpolants entails significant advantages, that motivate its practical usage. This talk provides an overview of SAT-based bounded model checking and of the utilization of interpolants in unbounded model checking. Moreover, improvements to the original interpolant-based unbounded model checking algorithm are described.
Tuesday 6th December 2005, 14:00
Robert Recorde Room
Department of Computer Science