SM/0122/EN - FORMAL METHODS
Academic Year 2022/2023
Free text for the University
GIOVANNI MICHELE PINNA (Tit.)
- Teaching style
- Lingua Insegnamento
|[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.
The course does not require any specific knowledge beside the ones acquired in a laurea triennale in Computer Science.
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
Lectures are given mainly using blackboard. Other online material could be possibly used. 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.
Compatibly with the mixed teaching method foreseen in the Academic Manifesto for the A.Y. 2020-21 following the COVID-19 emergency, the tools used for the lectures will be both the blackboard and tablet with projection system via classroom screen and via internet streaming.
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.
Accordingly to the Manifesto of Studies for the A.Y. 2021-22 following the COVID-19 emergency, lessons will be mainly given in class, integrated and augmented with online strategies, to assure the correct and fruitful attendance. Exams will follow the same guidelines.
Christel Baier & Joost-Pieter Katoen: Principles of Model Checking, MIT Press
Some videos with some additional lectures will be prepared, if needed.