Academic Year 2022-2023



Angelo Montanari
Gabriele Puppis
Luca Geatti
Unit Credits
Teaching Period
Second Period
Course Type
Prerequisites. The basic notions of algorithms and data structures, computability theory, mathematical logic, formal methods, automata theory, and formal languages. In the first part of the course, we will recall some basic notions and results about logic, automata theory, and games theory.
Teaching Methods. Most of the classes will be classroom-taught lessons and will make use of the blackboard and/or of slides. Some lessons will be devoted to the presentation of existing automated verification systems. The discussion of the solutions to the exercises given by the students is an integral part of the course. The writing of a technical relation and the subsequent oral presentation of its contents aim at promoting the ability of analyzing a scientific contribution in a critical way as well as of presenting the outcomes of such an analysis in a systematic and clear way.
Verification of Learning. The evaluation of the student’s understanding consists of the following complementary parts. During the semester, the student is invited to solve in an autonomous way a number of exercises associated with the different topics of the course. The oral examination will start with these exercises and will possibly involve all the topics addressed in the course. In addition, the student must study in detail a specific subject, selected together with the instructor, related to the topics of the course. The results of such a study must be described in a written report and presented by a seminar. The student can replace such a theoretical study by a more practical one consisting of, for instance, an experimental analysis of one of the existing verification systems or the development and implementation of a specific software module.
The course aims at providing a systematic account of computer science methods, formalisms, and algorithms for the formal specification and automatic verification/validation of complex reactive systems. The student will learn how to master advanced formal tools (logic, automata theory, logical game theory) to be used for the analysis and the automatic verification of complex systems.
The course aims at providing a systematic account of computer science methods, formalisms, and algorithms for the formal specification and automatic verification/validation of complex reactive systems and their use in the areas of artificial intelligence and cybersecurity. A prominent role is assigned to the theory of automata operating on infinite objects (words and trees) and to temporal logics (LTL, CTL, CTL*, mu-calculus). A special attention is given to the expressive equivalence between classes of automata and logical systems. The possible role of the logical theory of games in formal verification is illustrated as well. From the algorithmic point of view, on the basis of the considered computational models and specification formalisms, the course studies in detail the main algorithms for specification consistency checking (satisfiability checking) and model checking. A special emphasis is given to model checking algorithms, that make it possible to validate the behaviour of hardware and software systems, modelled by means of a suitable mathematical model, e.g., an automaton, with respect to their formal requirements, specified by means of logical formulas, e.g., CTL formulas. In particular, the course described the main achievements in improving the performance of model checking algorithms (symbolic model checking, OBDD, partial order reduction). Moreover, a short account of meaningful examples of model checkers is given. In addition, some advanced topics are briefly introduced such as, for instance, the synthesis problem. In the last part of the course, we describe some applications of considered techniques and tools to automated planning and symbolic verification of cryptographic protocols.
Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer, 1992.

Z. Manna, A. Pnueli. Temporal Verification of Reactive Systems: Safety, Springer, 1995.

A. Montanari, Formal languages, automata, and logics, Lecture Notes, 2020.

W. Thomas. Automata on Infinite Objects, in Handbook of Theoretical Computer Science – Vol. B (Chapter 4), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.

W. Thomas. Languages, Automata, and Logic, in Handbook of Formal Languages, Vol. III, G. Rozenberg and A. Salomaa (eds.), Springer, pp. 389-455, 1997.

D. Perrin, J.-E. Pin, Infinite Words. Automata, Semigroups, and Games, Pure and Applied Mathematics Vol. 141, Elsevier, 2004.

E. A. Emerson. Temporal and Modal Logic, in Handbook of Theoretical Computer Science Vol. B (Chapter 16), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.

E. M. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, 2000.

W. Thomas, Solution of Church’s Problem: A Tutorial, 2009.