PhD in Computer Science

Model checking

Model checking

Academic year 2018/2019

Sommario del corso

• Results of learning outcomes
• Learning assessment methods
• Program
• Suggested textbooks and readings
• Teaching tools

Results of learning outcomes

Students of the course will have both a theoretical and practical grounding in the field of model checking: with regard to theory, the students will learn fundamental concepts related to model checking; with regard to practice, they will obtain hands-on experience of using model checking tools to model and verify case studies from various contexts. Therefore the students will obtain both the conceptual and practical knowledge of how to employ model checking to detect and modify errors or inefficiencies in system designs.

Learning assessment methods

The exam has to be agreed on with the lecturer, but will principally  comprise "hands-on" exercises with verification tools together with an  theoretical analysis of a topic either not considered in depth during  the course, or on a topic considered more exhaustively, in which case  there will be a focus on the implications of the topic for the field of  research of the student.

Program

It is widely acknowledged that problems detected early in the system development process are less expensive to fix than those detected later. Formal modelling and verification techniques can be used to detect errors or inefficiencies in the design phase, allowing us to thoroughly check and understand a system design before its construction. Model checking is a widespread verification technique that consists in the automatic (push-button) and exhaustive analysis of a formal system model against a set of formally specified correctness requirements. Model checking techniques have been used in a wide variety of application contexts, ranging from circuits and network protocols to biological systems and autonomous systems interacting with human operators. This course will give an introduction to the field of model checking, and will comprise the following topics: classical model checking of finite-state systems against temporal logic specifications (Donatelli); symbolic data structures for the efficient representation of systems in model checking analyses (Beccuti); model checking for quantitative properties, in particular model checking for timed and probabilistic systems (Sproston). During the course the various topics will be illustrated by case studies for a number of application contexts, and students will have the opportunity to use model checking tools.

Principles of Model Checking
Autore: Christel Baier and Joost-Pieter Katoen
Casa editrice: MIT Press
ISBN: 9780262026499

• Teaching materials
• Exams and finals
• Go to Moodle
• Visit the forums