Formal Methods in Software Development

teacher: Anna Labella

a.a. 2016-17

Teacher Anna Labella
Phone 06 4925(3)5159
Appointments via email
| Office | V.le Regina Elena 295 pal. G, room G 39

Lectures timetable

Time table Classroom
Mon. and Wed. 8.30-10.00 Aula Alfa (via Salaria, 113)

Notifications: lectures will begin on Monday the 20th of February 2017 at 8:30 in classroom Alfa

Suggested readings

M. Huth, M. Ryan "Logic for Computer Science" Cambridge, ©2004,
J.-F. Monin "Understanding formal methods" Springer, ©2003
M. Ben-Ari "Mathematical Logic for Computer Science" Springer, ©2012
Some notes will be delivered by the teacher on specific topics


  • Temporal Logics and Model checking
  • Hoare logic and verification of programs
  • Reactive Systems and Hennessy-Milner logic
  • Order structures and Denotational semantics

Examination modalities

  • A project in collaboration and an oral examination on part of the program, or
  • An oral examination on all the program
  • The oral examination on part of the program can be substituted by an intermediate written test

Project modalities:

* Students can form groups of 2 up to 4 members.

* The project work is divided as follows:

1. By the end of the last lesson on system modelling, each group will be assigned a computer system to be formally modelled and verified by making use the NuSMV model checker. A description of the system can be either taken from an external source (e.g., research paper, Wikipedia), or defined by the tutor.By the end of the last lesson on system modelling, each group will be assigned a computer system to be formally modelled and verified by making use the NuSMV model checker. A description of the system can be either taken from an external source (e.g., research paper, Wikipedia), or defined by the tutor.

2. The group will start refining a model of the system through the analysis and definition of logical properties that have to be met by such a model. Each member of the group should define at least one safety property as well as one liveness property. [30% of the project grade].

3. Both model and logical properties have to be written in NuSMV input language in order to be formally verified. The NuSMV model checker will basically​ ​tell whether or not each property is satisfied by the model. Until no more refinements on the model are needed, (which means every property is satisfied as expected,) steps 2 and 3 have to be repeated. [40% of the project grade]

4. During the final examination date, each group will be invited to make a short presentation (10 minutes) on the work done. [30% of the project grade]


* Slides from the lectures will be at disposal on this spage *

* Lesson_1.20_2_2017.ppt: first lesson

* Lesson_2.22_2_2017_.pptx: second lesson

Useful Links

Topic attachments
I Attachment History Action Size Date Who Comment
PowerPointppt Lesson_1.20_2_2017.ppt r1 manage 551.5 K 2017-02-21 - 07:16 AnnaLabella first lesson
PowerPointpptx Lesson_2.22_2_2017_.pptx r1 manage 211.9 K 2017-02-23 - 11:34 AnnaLabella second lesson
PowerPointppt Lezione1.5_3_2014.ppt r2 r1 manage 330.5 K 2014-03-12 - 13:19 AnnaLabella prima lezione
PowerPointppt Lezione13.28-04-2014.ppt r1 manage 3869.0 K 2014-04-28 - 14:32 AnnaLabella tredicesima lezione
PowerPointppt Lezione14.30_4_2014.ppt r1 manage 933.5 K 2014-05-02 - 06:33 AnnaLabella Quattordicesiam lezione
PowerPointppt Lezione15.5-5-2014.ppt r2 r1 manage 1347.5 K 2014-05-18 - 09:57 AnnaLabella quindicesima lezione
PowerPointppt Lezione16.7-5-2014.ppt r2 r1 manage 2040.0 K 2014-05-18 - 10:19 AnnaLabella sedicesima lezione
PowerPointppt Lezione17.12-5-2014.ppt r2 r1 manage 629.5 K 2014-05-18 - 10:27 AnnaLabella diciassettesima lezione
PowerPointppt Lezione18.14-5-2014.ppt r2 r1 manage 824.0 K 2014-05-18 - 10:28 AnnaLabella diciottesima lezione
PowerPointppt Lezione_11.27_4_2015.ppt r1 manage 2384.5 K 2016-04-27 - 08:51 AnnaLabella eleventh lesson
PowerPointppt Lezione_19.19-5-2014.ppt r1 manage 3580.5 K 2014-05-19 - 12:07 AnnaLabella diciannovesima lezione
PowerPointpptx Lezione_2.10_3_2014.pptx r2 r1 manage 166.1 K 2014-03-12 - 13:20 AnnaLabella seconda lezione
PowerPointppt Lezione_20.21-5-2014.ppt r1 manage 2897.5 K 2014-05-21 - 10:18 AnnaLabella ventesima lezione
PowerPointppt Lezione_21.26-5-2014_.ppt r1 manage 775.5 K 2014-05-26 - 13:04 AnnaLabella ventunesima lezione
PowerPointppt Lezione_22.28-5-2014.ppt r1 manage 1753.0 K 2014-05-29 - 07:00 AnnaLabella ventiduesima lezione
PowerPointppt Lezione_23_(es).4-6-2014.ppt r1 manage 279.5 K 2014-06-07 - 03:59 AnnaLabella Esercitazione sulla seconda parte
PowerPointpptx Lezione_3.12_3_2014_.pptx r3 r2 r1 manage 348.0 K 2014-03-17 - 18:10 AnnaLabella terza lezione
PowerPointpptx Lezione_4.17_3_2014__.pptx r3 r2 r1 manage 116.8 K 2014-03-18 - 07:32 AnnaLabella quarta lezione
PowerPointppt Lezione_5.19-3-2014.ppt r1 manage 621.0 K 2014-03-20 - 18:42 AnnaLabella quinta lezione
PowerPointppt Lezione_6.24-3-2014.ppt r1 manage 603.0 K 2014-03-24 - 14:15 AnnaLabella sesta lezione
PowerPointppt Lezione_7.26-3-2014_.ppt r1 manage 445.0 K 2014-03-27 - 07:03 AnnaLabella settima lezione
PowerPointppt Lezione_8.31-3-2014_.ppt r1 manage 1357.0 K 2014-04-01 - 14:03 AnnaLabella ottava lezione
PowerPointppt Lezione_9_(es).2-4-2014.ppt r1 manage 356.0 K 2014-04-03 - 07:45 AnnaLabella nona lezione
Microsoft Word filedocx Risultati_17062014.docx r1 manage 53.9 K 2014-06-17 - 18:08 AnnaLabella Risultati scritto giugno 2014
PDFpdf appunti_semantica.pdf r1 manage 3039.1 K 2014-05-02 - 06:38 AnnaLabella dispense
PDFpdf intro2ccs.pdf r1 manage 504.5 K 2014-06-05 - 12:53 AnnaLabella dispense Su CCS e Hennessy Milner logic
Edit | Attach | Watch | Print version | History: r62 < r61 < r60 < r59 < r58 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r62 - 2017-02-23 - AnnaLabella

Questo sito usa cookies, usandolo ne accettate la presenza. (CookiePolicy)
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback