OTHER ACADEMIC YEARS

Automated Verification of Cyber-Physical Systems

Master Degree in Computer Science

University of L'Aquila

A.Y. 2024/2025

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 12/06/2025 11:00 - 13:00 C1.16 Please discuss the project/paper with the lecturer in advance 08/06/2025 h23:59:59
2 26/06/2025 11:00 - 13:00 Please discuss the project/paper with the lecturer in advance 22/06/2025 h23:59:59
3 10/07/2025 11:00 - 13:00 Please discuss the project/paper with the lecturer in advance 06/07/2025 h23:59:59
4 04/09/2025 11:00 - 13:00 Please discuss the project/paper with the lecturer in advance 31/08/2025 h23:59:59
5 15/01/2026 11:00 - 13:00 Please discuss the project/paper with the lecturer in advance 11/01/2026 h23:59:59
6 29/01/2026 11:00 - 13:00 Please discuss the project/paper with the lecturer in advance 25/01/2026 h23:59:59
7 12/02/2026 11:00 - 13:00 Please discuss the project/paper with the lecturer in advance 08/02/2026 h23:59:59

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 25/02/2025 slides Presentation of the course. Introduction to classical model checking techniques Slides 1-69
2 27/02/2025 see Lecture 1 Introduction to classical model checking techniques (contd) Slides 70-122
3 04/03/2025 see Lecture 1 Introduction to classical model checking techniques (finished) Slides 123-end
4 06/03/2025 slides Probabilistic Model Checking (part 1) Slides 1-80
5 11/03/2025 See lesson 4 Probabilistic Model Checking (part 2) Slides 81-108
6 13/03/2025 See lesson 4 Probabilistic Model Checking (part 3) Slides 109-151
7 18/03/2025 See lesson 4 Probabilistic Model Checking (part 4) Slides 152-184
8 20/03/2025 See lesson 4 Probabilistic Model Checking (part 5) Slides 185-219
25/03/2025 CANCELED
9 27/03/2025 See lesson 4 Probabilistic Model Checking (part 6) Slides 220-247
10 01/04/2025 See lesson 4 Probabilistic Model Checking (part 7) Slides 248-307
11 03/04/2025 See lesson 4 Probabilistic Model Checking (part 8) Slides 308-359
12 08/04/2025 See lesson 4 Probabilistic Model Checking (part 9) Slides 360-end
13 10/04/2025 slides
examples in Modelica		 Simulation of CPSs (part 1) Slides 1-40
14 15/04/2025 See lesson 13 Simulation of CPSs (part 2) Slides 41-68
15 24/04/2025 See slides in lesson 13
slides		 Simulation of CPSs (part 3). Statistical Model Checking (part 1) Slides 69-end. Slides 1-10
16 29/04/2025 See slides of lesson 15 Statistical Model Checking (part 2) Slides 11-41
17 06/05/2025 See slides of lesson 15 Statistical Model Checking (part 3) Slides 42-81
18 08/05/2025 See slides of lesson 15 Statistical Model Checking (part 4) Slides 82-115
19 13/05/2025 See slides of lesson 15 Statistical Model Checking (part 5). Introduction to project and papers for the exam Slides 116-end
20 15/05/2025 Review of students' projects/papers
21 20/05/2025 Review of students' projects/papers
22 22/05/2025 Review of students' projects/papers
23 27/05/2025 Review of students' projects/papers
24 29/05/2025 Review of students' projects/papers

Class Timetable

Day From To Where
Tuesday 9:30AM 11:30AM Digital Class
Thursday 9:30AM 11:30AM A.0.6

Room A.0.6 is at the first floor of the "Renato Ricamo" building; it may be reached from the outside only.

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

Free software for this course