OTHER ACADEMIC YEARS

Index:

Exams

Course programme

Textbooks

Class material

Class timetable

Exams

Exams Rules

See lesson 1.

Exams Dates

N	Date	Hour	Where	Notes	Deadline
1	06/2026
2	06/2026
3	07/2026
4	09/2026
5	01/2027
6	01/2027
7	02/2027

Official information is here

Course Programme

Cyber-Physical Systems Modeling and Simulation

• Modelica and Simulink

Statistical Model Checking

• modeling and algorithms

Probabilistic Model Checking

• modeling and algorithms
• PRISM

System Level Formal Verification

• modeling and algorithms

Textbooks:

• Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem (Editors): Handbook of Model Checking, Springer
• A version of this book is available here

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 Lecture 1	Introduction to classical model checking techniques (contd)	Slides 59-92
3	03/03/2026	see Lecture 1	Introduction to classical model checking techniques (contd)	Slides 93-127
4	05/03/2026	see Lecture 1	Review of the past lessons
5	10/03/2026	see Lecture 1	Introduction to classical model checking techniques (contd)	Slides 128-170
6	12/03/2026	see Lecture 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

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

• CMurphi
• SPIN
• NuSMV