Model Checking

Overview

Content

Model checking is a technique used for automatically verifying whether hardware or software systems meet a given specification. Model checking has made enormous progress during the last 20 years and is nowadays used in large- scale industrial applications. This course teaches the fundamentals of model checking, mostly for systems with finite state spaces. The course starts with the basics behind temporal logics (LTL, CTL), used for specifying correctness properties. Hardware or software systems of interest are modelled as Kripke structures, and it will be shown how such structures can be efficiently extracted, e.g., from the source code of a program. The course incorporates basic verification algorithms as well as various optimizations (“On-the-fly” model checking, partial-order reduction, binary decision diagrams, abstraction/refinement, bounded model checking) and gives a vivid picture of the current state-of-the-art. The techniques taught in the course are illustrated by software tools (Spin, SMV, Blast, CBMC), and participants have opportunity of getting hands-on experience with these.