Formal Methods

Prof. Giuseppe De Giacomo

A.A. 2021/22

Announcements:

  • The Formal Methods lectures will start on Monday Sept. 27, 2021, 15:00-19:00, Aula 11 Economia.

  • The Formal Methods lecture on Wednesday Sept. 29, 2021 is cancelled.

  • From Monday Oct. 11, 2021 the 15:00-19:00 lectures are moved to room A5 in Via Ariosto 25.

  • The lectures of Wednesday Dec. 15 and Dec. 22, 2021 will be given only online.

  • Final Test on Monday Dec. 20, 2021 (register below).

Final Test on Monday December 20, 2021 at 15:00

Please register here by Dec. 15, 2021:

Registration Form for the Final Test


To get access please use your account studenti.uniroma1.it




Welcome

The lectures of Formal Methods 2021/2022 (Prof. De Giacomo) will start on Monday Sept. 27, 2021 and end on Wednesday Dec. 22, 2021. The course is scheduled Mondays from 15:00 to 19:00 in AULA 11 Economia and Wednesdays from 17:00 to 19:00 in AULA 3 blu CU028.

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.

Course Description

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. The course will introduce various forms of logic (first-order logic, 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 2021/2022 and additional readings available in this page.

Lectures: Mondays from 15:00 to 19:00 in AULA 11 Economia and Wednesdays from 17:00 to 19:00 in AULA 3 blu CU028.

Zoom room for the lectures

The Zoom room for the attending lectures online is the following:

https://uniroma1.zoom.us/j/7737376235


To get access please use your account studenti.uniroma1.it