Formal Methods

The lectures of Formal Methods 2023/2024 (Prof. De Giacomo) will start on Thursday, Sept. 28, 2023, and end on Friday, Dec. 22, 2023.  The course is scheduled on Thursdays from 16:00 to 20:00 and Fridays from 18:00 to 20:00 in AULA A4 Via Ariosto 25. Some of the lectures will be online. 

The course can be chosen by 2nd year students, and 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! 

Please do not forget to register for the forum of the course. Communication will happen through the forum.

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 2023/2024 and additional readings available on this page. 

Lectures: Thursdays from 16:00 to 20:00 and Fridays from 18:00 to 20:00 in AULA A4 Via Ariosto 25.