Automated System Verification (2015/2016)

Course code
Name of lecturers
Nicola Fausto Spoto, Alessandro Cimatti
Nicola Fausto Spoto
Number of ECTS credits allocated
Academic sector
Language of instruction
II semestre dal Mar 1, 2016 al Jun 10, 2016.

Lesson timetable

II semestre
Day Time Type Place Note
Monday 2:30 PM - 5:30 PM lesson Lecture Hall I  
Tuesday 2:30 PM - 4:30 PM lesson Laboratory Laboratorio Ciberfisico from Mar 15, 2016  to Jun 10, 2016
Tuesday 4:30 PM - 6:30 PM lesson Lecture Hall I  

Learning outcomes

The course presents problems related to the verification of complex systems and its related techniques.


The course introduces the problem of modeling complex and highly critical systems, such as railway systems, avionics, spatial and project control systems, and the related requirements. It presents transition systems and their symbolic representation as propositional logic. It presents temporal logic: Computation Tree Logic, Linear Temporal Logic and CTL*. It describes algorithms for model checking verification of CTL and the generalization to transition systems with fairness constraints. It presents the translation of LTL model checking into CTL model checking with fairness constraints. It presents symbolic algorithms for model checking, based on Binary Decision Diagrams (BDD), and algorithms based on propositional satisfiability (SAT). It describes aspects of reliability and analysis of systems with Triple Modular Redundancy (TMR), Fault Tree Analysis notions and algorithms to compute the cut sets and for minimization. It presents the notions of abstraction, refinement and predicate abstraction. It describes temporal systems and hybrid automata and related decidability issues. The course is integrated with exercises with the use of a BDD package and of the model checker NuSMV.

Assessment methods and criteria

Oral examination or software project

Teaching aids