OTHER ACADEMIC YEARS

Automated Verification of Cyber-Physical Systems

Master Degree in Computer Science

University of L'Aquila

A.Y. 2025/2026

lecturer: Igor Melatti

igor.melatti@univaq.it

Index:

Exams

Course programme

Textbooks

Class material

Class timetable

Exams

Exams Rules

See lesson 1.

Available Papers

The following papers may be used for the paper-related exam:

Available Projects

Available projects are described in this document.

Exams Dates

N Date Hour Where Notes Deadline
1 18/06/2026 12:00PM - 1:00PM Please discuss the project/paper with the lecturer in advance 14/06/2026 h23:59:59
2 02/07/2026 12:00PM - 1:00PM Please discuss the project/paper with the lecturer in advance 28/06/2026 h23:59:59
3 16/07/2026 5:00PM - 6:00PM Please discuss the project/paper with the lecturer in advance 12/07/2026 h23:59:59
4 10/09/2026 12:00PM - 1:00PM Please discuss the project/paper with the lecturer in advance 06/09/2026 h23:59:59
5 01/2027
6 01/2027
7 02/2027

Official information is here

Course Programme

Cyber-Physical Systems Modeling and Simulation

Statistical Model Checking

Probabilistic Model Checking

System Level Formal Verification

Textbooks:

Scientific papers provided by the lecturer

Class Material

N Date Material Arguments Notes
1 24/02/2026 slides Presentation of the course. Introduction to classical model checking techniques Slides: 1-58
2 26/02/2026 see lesson 1 Introduction to classical model checking techniques (contd) Slides 59-92
3 03/03/2026 see lesson 1 Introduction to classical model checking techniques (contd) Slides 93-127
4 05/03/2026 see lesson 1 Review of the past lessons
5 10/03/2026 see lesson 1 Introduction to classical model checking techniques (contd) Slides 128-170
6 12/03/2026 see lesson 1 Introduction to classical model checking techniques (finished) Slides 171-end
7 17/03/2026 slides Probabilistic Model Checking (part 1) Slides 1-71
8 19/03/2026 See lesson 7 Probabilistic Model Checking (part 2) Slides 72-102
9 24/03/2026 See lesson 7 Probabilistic Model Checking (part 3) Slides 103-188
10 26/03/2026 See lesson 7 Probabilistic Model Checking (part 4) Slides 189-243
11 31/03/2026 See lesson 7 Probabilistic Model Checking (part 5) Slides 244-313
12 09/04/2026 See lesson 7 Probabilistic Model Checking (part 6) Slides 314-368
13 14/04/2026 See lesson 7 Probabilistic Model Checking (part 7) Slides 369-end
14 16/04/2026 slides Simulation of CPSs (part 1) Slides 1-39
15 21/04/2026 examples in Modelica Simulation of CPSs (part 2) Slides 40-70
16 23/04/2026 See lesson 15 Simulation of CPSs (part 3) Slides 71-end
17 28/04/2026 slides Statistical Model Checking (part 1) Slides 1-28
18 30/04/2026 See lesson 17 Statistical Model Checking (part 2) Slides 29-100
19 05/05/2026 See lesson 17 Statistical Model Checking (part 3). Introduction to project and papers for the exam Slides 101-end
20 07/05/2026 Review of students' projects/papers
21 12/05/2026 Review of students' projects/papers
22 14/05/2026 Review of students' projects/papers
23 19/05/2026 Review of students' projects/papers
24 21/05/2026 Review of students' projects/papers

Class Timetable

Day From To Where
Tuesday 9:30AM 11:30AM Digital Class
Thursday 9:30AM 11:30AM Mathematical Modeling Laboratory

The Digital Class is immediately outside the "Alan Turing" building, in a separate small house.

The Mathematical Modeling Laboratory is inside the "Ricamo" bulding: immediately before going out towards the "De Meis" building, turn left (there is a "DISIM" sign) and go to the very last door on the right.

Free software for this course