Select Academic Year:     2017/2018 2018/2019 2019/2020 2020/2021 2021/2022 2022/2023
First Semester 
Teaching style
Lingua Insegnamento

Informazioni aggiuntive

Course Curriculum CFU Length(h)
[60/73]  INFORMATICS [73/00 - Ord. 2017]  PERCORSO COMUNE 6 48


1. Acquiring knowledge and understanding
The course, devoted to second year students of the Laurea Magistrale in Computer Science, has as main target the achievement of all the knowledges, both theoretical and practical, that will allow the complete comprehension and their effective applicability of the design and verification, using model checking techniques, of a complex system.

2. Applying knowledge and understanding
The course will illustrate methodologies concerning system modeling, and how to formulate and effectively verify
properties the system should enjoy.

3. Making informed judgements and choices
The course provides all the tools and notions to face critically every problem connected to the modeling and
verification of complex systems.

4. Communicating knowledge and understanding
The written proof, with open questions, allows the student to show his capability of exposing in a clear and
coherent manner the treated arguments.

5. Learning capabilities
The course gives an adequate background to be able to face all the problems concerning the design,
development and implementation of programming languages, and gives the key notions to comprehend the
theory and applications of programming languages.


1. Knowledge
The course does not require any specific knowledge beside the ones acquired in a laurea triennale in Computer Science.

2. Skills
None specific.

3. Competence
None specific.

Preparatory courses:


The course is organized in 24 lessons concerning both the theory but also the application (each lesson presents an argument in the first part, and in the second part some examples, applications and exercises are provided).

Lessons are divided into three groups:

  • in the first group is devoted to the modeling of complex system (transition system), on how to represent the
    computations of a transition system, focussing on concurrency and parallelism, and on how to formalize properties one wish to verify for the system

  • the lessons the second group focus on the Linear Time Logic (LTL) and on how to do model checking for properties formalized using LTL

  • in the third group the Computational Time Logic (CTL) is formalized and investigated, in particular on how to do model checking for properties written in CTL, and which are the relations with LTL

Teaching Methods

Lectures are given using blackboard. No slides are used, as the book used contains the material illustrated during the lessons, and using the blackboard allows to explain better using the proper pace.

Verification of learning

For each lessons a number of exercise will be proposed, and together with a written exam, will be used in the oral exam.


Christel Baier & Joost-Pieter Katoen: Principles of Model Checking, MIT Press

More Information


Questionnaire and social

Share on:
Impostazioni cookie