Formal Methods

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 models.

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

Posts

In this section contingent information on the course will be posted, not information on office hours (for this please refer to the instractor teaching page.

• Lectures: Wednesday 14:00-15:30 (2 hours) and Thursday 15:45-19:00 (4 hours), Room A3, via Ariosto 25.
  
  
• Office hours: see instructor teaching page.
  
  
• Lecture diary
  
  
• Teaching material
  
  
• Course program
  

• aa2008/09
• aa2009/10
• aa2010/11
• aa2011/12
• aa2012/13
• aa2013/14

Exams

• The exam is written and deals with every aspects tought during the course.
• Previous exams.

• First session: reservation from 19/12/2014 to 18/01/2015 (Text and Results)
  • DATE: January 22, 2015
  • TIME: 15:00
  • ROOM: 12 and 13 Via Scarpa (we meet in room 12 and then split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is automatic. The correction of students' exam can be seen on Feb 10, 2015 and Feb 11, 2015 at 17:00, in the Instructor office (room B215 Via Ariosto 25). After that date the registration will be closed and sent to the administrative offices. Who does not want to register the result, and wants to take the exam again, can send to me an email from his/her official SAPIENZA account by Feb 11, 2015.
• Second session: reservation from 22/01/2015 to 15/02/2015 (Text and Results)
• DATE: February 18, 2015
• TIME: 15:00
• ROOM: 12 and 13 Via Scarpa (we meet in room 12 and then split)
• REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is automatic. The correction of students' exam can be seen on March 19, 2015 at 17:00, in the Instructor office (room B215 Via Ariosto 25). After that date the registration will be closed and sent to the administrative offices. Who does not want to register the result, and wants to take the exam again, can send to me an email from his/her official SAPIENZA account by March 19, 2015.
• Special session (appello straordinario): reservation from 01/03/2015 to 18/03/2015 (Results)
  Important: to take the exam in this session you need to formally conform to the following regulation (double check with administration if in doubt): "Gli appelli straordinari sono aperti solo agli studenti ripetenti, part-time, fuori corso o che abbiano completato comunque tutte le frequenze".
  • DATE: March 23, 2015
  • TIME: 16:00
  • ROOM: 13 Via Scarpa
  • REGISTRATION (verbalizzazione): Please notice that the registration of the exam (verbalizzazione) is automatic. The correction of students' exam can be seen on April 16, 2015 at 17:00, in the Instructor office (room B215 Via Ariosto 25). After that date the registration will be closed and sent to the administrative offices. Who does not want to register the result, and wants to take the exam again, can send to me an email from his/her official SAPIENZA account by April 16, 2015.
• Third session: reservation from 07/05/2015 to 07/06/2015 (Text and Results)
  • DATE: June 11, 2015
  • TIME: 15:00
  • ROOM: 12 and 13 Via Scarpa (we meet in room 12 and then split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is automatic. The correction of students' exam can be seen on June 18, 2015 at 17:00, in the Instructor office (room B215 Via Ariosto 25). After that date the registration will be closed and sent to the administrative offices. Who does not want to register the result, and wants to take the exam again, can send to me an email from his/her official SAPIENZA account by June 18, 2015.
• Fourth session: reservation from 11/06/2015 to 05/07/2015 (Text and Results)
  • DATE: July 9, 2015
  • TIME: 15:00
  • ROOM: 2 and 3 Via Scarpa (we meet in room 3 and then split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is automatic. The correction of students' exam can be seen on July 16, 2015 at 17:00, in the Instructor office (room B215 Via Ariosto 25). After that date the registration will be closed and sent to the administrative offices. Who does not want to register the result, and wants to take the exam again, can send to me an email from his/her official SAPIENZA account by July 16, 2015.
• Fifth session: reservation from 09/07/2015 to 06/09/2015 (Text and Results)
  • DATE: September 11, 2015
  • TIME: 15:00
  • ROOM: 2 and 3 Via Scarpa (we meet in room 3 and then split)
  • REGISTRATION (verbalizzazone): tba
• Special session (appello straordinario): reservation from 19/10/2015 to 09/11/2015 (Results)
  Important: to take the exam in this session you need to formally conform to the following regulation (double check with administration if in doubt): "Gli appelli straordinari sono aperti solo agli studenti ripetenti, part-time, fuori corso o che abbiano completato comunque tutte le frequenze".
  • DATE: November 11, 2015
  • TIME: 14:30
  • ROOM: 2, Via Scarpa
  • REGISTRATION (verbalizzazione):  tba