Formal Methods

The lectures of Formal Methods 2022/2023 (Prof. De Giacomo) will start on Friday Sept. 30, 2022 and end on Wednesday Dec. 23, 2022. The course is scheduled Mondays from 9:00 to 11:00 in AULA A3 and Fridays from 15:00 to 19:00 in AULA A4, Via Ariosto 25.

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

Please do not forget to register to 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, basic notions on propositional and first-order logic as acquired in previous years courses.

Objectives. The objective of the course is the study of the most important among the qualities of software: correctness. Correctness will be studies looking at the conceptual perspective as well as the realization perspective. Modeling and verification of dynamic (processes) aspects will be considered. The various topics will be treated emphasizing methodological, theoretical and practical facets. The course will introduce various forms of logic (linear temporal logics, branching temporal logics, fixpoint logics), techniques and tools for automated verification. After the successful completion of the course the student will have acquired techniques and methods for proving correctness of programs and conceptual process models.

Teaching material.

[1] Course slides 2022/2023 and additional readings available in this page.

Lectures: Mondays from 9:00 to 11:00 in AULA A3 and Fridays from 15:00 to 19:00 in AULA A4, Via Ariosto 25.