This course gives an introduction to model-checking, a technique for automatic verification of software and reactive, embedded systems. Model checking was invented long time ago, and has been used successfully in many industrial projects. Many researches in this topic are still in progress. This course will give the basic elements required for understanding model checking, and the basic skills for using model checking tools. It also provides the basic knowledge for the researchers to start doing research in this topic.
No special knowledge is required except for the computer science background.
The course lasts 3 days, i.e. 6 3-hour sessions.