Symbolic Model Checking
A Hands-On Introduction

- ESSLLI 2002 - Trento - 5-9 August, 2002 -


Alessandro CIMATTI and Marco PISTORE

ITC-IRST
Via Sommarive 18, 39055 Povo (TN) - Italy
{cimatti,pistore}@irst.itc.it

Description

Model Checking is a formal technique for the verification of finite-state concurrent systems. Symbolic Model Checking is a particular form of Model Checking that allows to analyze extremely large finite-state systems by means of symbolic representation techniques (e.g. Binary Decision Diagrams, propositional satisfiability). Symbolic model checkers such as SMV and VIS have been used to verify industrial systems, ranging from hardware to communication protocols to safety critical plants and procedures. Symbolic Model Checking is applied in technology transfer projects, and is the core technique for several industrial verification tools.

The aim of the course is to provide a basic understanding of the theory and of the practical techniques of Symbolic Model Checking. Following the successful experiment of the Floc'99 Model Checking Tutorial, the course combines theoretical and practical sessions. During the practical sessions, the participants will be confronted with a symbolic model checker and a set of problems, and will therefore acquire a hands-on experience.

The examples and notations used in the practical sessions, and the exercises proposed in the practical sections will be based on NuSMV, a model checker that provides (BDD-based and SAT-based) symbolic verification techniques. The course will give an introduction to SMV (the input language of NuSMV) and to the basic functionalities of NuSMV, so that the partcipants will be able to carry out simple simple design and verification tasks.

The course covers the following topics:

The gNuSMV program

A pre-release of gNuSMV can be found here.

NuSMV Manuals

Slides

LESSON 1 - Monday (Theory)

LESSON 2 - Tuesday (Hands-on)

LESSON 3 - Wednesday (Theory)

LESSONS 4 and 5 - Thursday and Friday (Hands-on)