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 2013/14 and additional readings available in this page.

Posts

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

• Lectures: Wednesday 10:15-11:45 (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

Exams

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

• First session: reservation from 01/01/2014 to 19/01/2014 (Text and Results)
  • DATE: January 22, 2014
  • TIME: 15:00
  • ROOM: Aula 12 & 13, Via Scarpa (we meet in aula 12 and then we split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Feb 11, 2014. 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 Feb 11, 2014.
• Second session: reservation from 23/01/2014 to 15/02/2014(Text and Results)
  • DATE: February 18, 2014
  • TIME: 9:30
  • ROOM: Aula 12 & 13, Via Scarpa (we meet in aula 12 and then we split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on March 4 and on March 11, 2014 at 17:00 during office hours. After that March 11, 2014 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 March 11, 2014.
• Special session (appello straordinario): reservation from 09/03/2014 al 06/04/2014 (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 9, 2014
  • TIME: 9: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 April 29, 2014 at at 17:00 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 Tuesday April 29, 2014.
• Third session: reservation from 09/05/2014 to 04/06/2014 (Text and Results)
  • DATE: June 9, 2014
  • TIME: 15:00
  • ROOM: Aula 12 & 13, Via Scarpa (we meet in aula 12 and then we split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on Wednesday June 25, 2014 at 12: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 Wednsday June 25, 2014 at 23:59.
• Fourth session: reservation from 10/06/2014 to 06/07/2014 (Text and Results)
  • DATE: July 9, 2014
  • TIME: 9:30
  • ROOM: Aula 12 & 13, Via Scarpa (we meet in aula 12 and then we split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on July 15, 2014 at 17:00 in Via Ariosto 25, room B215 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 July 15, 2014.
• Fifth session: reservation from 01/08/2014 to 09/09/2014(Text and Results)
  • DATE: September 12, 2014
  • TIME: 15:00
  • ROOM: Aula 3 &13, Via Scarpa (we meet in aula 13 and then we split)
  • REGISTRATION (verbalizzazone): Please notice that the registration of the exam (verbalizzazione) is now automatic. The correction of students' exam can be seen on October 7, 2014 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 October 7, 2014.
• Special session (appello straordinario): reservation from 01/10/2014 al 09/11/2014 (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 12, 2014
  • TIME: 16:00
  • ROOM: Aula 13, Via Scarpa
  • REGISTRATION (verbalizzazione):  Please notice that the registration of the exam (verbalizzazione) is now automatic. 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 Nov 28, 2014.