Formal Methods

Welcome to the site of Formal Methods 2025/2026 (Prof. De Giacomo).

The lectures will start on 25/09/2025 and end on 19/12/2025.  The course is scheduled on Thursdays and Fridays from 17:00 to 19:30 in AULA ZZZ Via Ariosto 25.

The course can be chosen by 2nd-year students. MSc Theses on the themes of the course are available. 

From now on, on this page, you'll find all the required information. Enjoy the course! 

Prerequisites. Students taking this course should have knowledge of software modeling and design, relational databases, and basic notions of propositional and first-order logic as acquired in previous years' courses. 

Objectives. The course's objective is to study the most important of the qualities of software: correctness. Correctness will be studied by looking at the conceptual perspective as well as the realization perspective. Modeling and verification of both static (data) and dynamic (processes) aspects will be considered. The various topics will be treated by emphasizing methodological, theoretical, and practical facets. The course will introduce various forms of logic (special fragments of first-order logic, linear temporal logics, branching temporal logics, fixpoint logics), techniques, and tools for automated verification. After successfully completing the course, the student will have acquired techniques and methods for proving the correctness of programs as well as conceptual process models. 

Teaching material. 

[1] Course slides 2025/2026 and additional readings are available on this page. 

Lectures: Thursdays and Fridays from 17:00 to 19:30 in AULA A4, Via Ariosto 25