SAPIENZA Università di Roma, MSc in Engineering in Computer Science
(Laurea Magistrale in Ingegneria Informatica)

Formal Methods

Prof. Giuseppe De Giacomo

Prerequisites. Students taking this course should have knowledge of object oriented analysis, modeling and design, relational databases, basic notions on 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 both static (data) and dynamic (processes) aspects will be considered. The various topics will be treated emphasizing methodological, theoretical and practical facets, making use of various forms of logic (first-order logic, description logics, temporal logics, fixpoint logics) and 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 models.

Teaching material.
[1] Course slides 2012/13 and additional readings available in this page.

Academic Year 2012/13

(Course given in the first semester: October 1, 2012 - December 21, 2012)


In this section contingent information on the course will be posted.

Key Information
Previous editions of the course


Exams calendar

back to Giuseppe De Giacomo' teaching page