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

Posts

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

• Room on Thursday moved to A3.
• Wednesday Oct. 17 and Thursday Oct. 18 there will be no Formal Methods lessons.
• I strongly recommend students of the course to attend the seminar Turing and Artificial Intelligence by Luigia Carlucci Aiello, December 4, 2012 - 16:30 - Aula Magna
• I strongly recommend students of the course to attend the seminar Database Queries: Logic and Complexity by Moshe Vardi, December 11, 2012 - 10:30 - Aula Magna
• The lesson of Thursday December 13, 2012 is cancelled.

• Lectures: Wednesday 10:15-11:45 (2 hours) room A4 e 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

Exams

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

• First session: reservation from 04/01/2013 to 20/01/2013 (Final Test Results and 22/01/2013 Text and Results)
  • DATE: January 22, 2013
  • TIME: 15:00
  • ROOM: Aula 12, Via Scarpa
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Tuesday Feb. 5, 2013, 17:00-19:00. 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 from his/her official SAPIENZA account by Friday Feb. 8, 2013.
• Second session: reservation from 23/01/2013 to 20/02/2013 (Text and Results)
  • DATE: February 22, 2013
  • TIME: 9:30
  • ROOM: Aula 12, Via Scarpa
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Tuesday Mar. 19, 2013 and Tuesday Mar. 26, 2013from 17:00 to 19:00. 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 from his/her official SAPIENZA account by Friday Mar. 27, 2013.
• Special session (appello straordinario): reservation from 23/03/2013 al 15/04/2013 (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: April 17, 2013
  • TIME: 15:30
  • ROOM: Aula 8, Via Eudossiana
  • REGISTRATION (verbalizzazione): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Tuesday May 7, 2013 from 17:00 to 19:00 and Friday May 10, 2013 on appointment. 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 from his/her official SAPIENZA account by Friday May. 10, 2013.
• Third session: reservation from 20/05/2013 to 04/06/2013 (Results)
  • DATE: June 7, 2013
  • TIME: 15:00
  • ROOM: Aula 12, Via Scarpa
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Tuesday June 11, 2013 from 17:00 to 19:00. 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 from his/her official SAPIENZA account by Friday June 14, 2013.
• Fourth session: reservation from 07/06/2013 to 04/07/2013 (Results)
  • DATE: July 9, 2013
  • TIME: 9:00
  • ROOM: Aula 12, Via Scarpa
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Thursday July 18, 2013 at 11:00. 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 from his/her official SAPIENZA account by Thursday July 18, 2013.
• Fifth session: reservation from 09/07/2013 to 09/09/2013 (Results)
  • DATE: September 13, 2013
  • TIME: 15:00
  • ROOM: Aula 13, Via Scarpa
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Thursday Sept 26, 2013 at 15:00. 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 from his/her official SAPIENZA account by Thursday Sept 26, 2013.
• Special session (appello straordinario): reservation from 01/10/2013 al 31/10/2013 (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: October 30, 2013
  • TIME: 15:00
  • ROOM: Aula 1, Via Scarpa
  • REGISTRATION (verbalizzazione): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on 12/11/13 during office hours. 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 from his/her official SAPIENZA account by 15/11/13.