FormalMethodsInSoftwareDevelopmentBefore2019 < MFS

---+!! Formal Methods in Software Development

teacher: Anna Labella
---++ a.a. 2018-19

<table border="2"> <tbody> <tr valign="top"> <td width="80%">

| *Teacher* | Anna Labella |||
| *Phone* | 06 4925(3)5159 |||
| *Appointments* | via email |||
| *Office* | V.le Regina Elena 295
pal. G, room G 39
| *Email* | labella@di.uniroma1.it  |||
| *Teaching assistants* | Federico Mari, Vadim Alimguzhin |||
http://federicomari.name/, federico.mari@uniroma4.it, alimguzhin@di.uniroma1.it

----
---++ Lectures timetable

<center>

| *Time table*  | *Classroom* |
| Mon. and Wed. 8.00-10.30 | Aula 2, via del Castro Laurenziano, 7a |
</center>

----
---++ Notifications:
 * <b> The first date devoted to the exposition of [FMSD] projects is fixed on the 28th of June at 11:00 in my room G39 viale Regina Elena, 295, building G, 2nd floor<br /></b>

 * <b>WARNING! All the lessons will begin at 8:30am<br /></b>

* *Lessons will start on Monday 25th of February* <br />

* *There will be no lesson on Wednesday 24th of April* <br />

* *There will be no lesson on Monday 13th of May* <br />

* *There will be no lesson on Monday 27th of May* <br />

----
---++ Suggested readings

| M. Huth, M. Ryan "Logic for Computer Science" Cambridge, ©2004, www.cs.bham.ac.uk/research/lics/ |
| 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 |
----
---++ Program

   * *Natural deduction*
   * *Temporal Logics and Model checking*
   * *Order structures and Denotational semantics*
   * *Reactive Systems and Hennessy-Milner logic*
   * *Hoare logic and verification of programs*
   * *Modelling practices (with Federico Mari and Vadim Alimguzhin)* <hr />
---++ Examination modalities

   * A project in collaboration and an oral examination on a part of the program, or
   * An oral examination on all the program
   * The oral examination on part of the program can be substituted by exercises performed during the lessons<br /> <p> </p>
---++ Modelling practices (with Federico Mari and Vadim Alimguzhin):

--- This unit addresses the use of formal methods for mathematical modelling of dynamical systems and for specification of logic properties involving time. Many techniques for model based analysis are critically studied through journal club activity. Students are engaged in computer laboratory activity on analysis and design of models taken from literature.

----

---++ Lectures (Slides from the lectures will be at disposal on this page)

 * a.y 2018/19 *

   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_1.25_2_2019.ppt][Lesson_1.25_2_2019.ppt]]: first lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_2.27_2_2019_.pptx][Lesson_2.27_2_2019_.pptx]]: second lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_3.4_3_2019_.pptx][Lesson_3.4_3_2019_.pptx]]: third lesson a.y. 2018/2019 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_4.6_3_2019.pptx][Lesson_4.6_3_2019.pptx]]: fourth lesson a.y. 2018/2019 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_5.11_3_2019.ppt][Lesson_5.11_3_2019.ppt]]: fifth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_6.13-3-2019.ppt][Lesson_6.13-3-2019.ppt]]: sixth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_7.18-3-2019.ppt][Lesson_7.18-3-2019.ppt]]: seventh lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_8.20-3-2019.ppt][Lesson_8.20-3-2018.ppt]]: eighth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_9.25-3-2019.ppt][Lesson_9.25-3-2019.ppt]]: ninth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_10.27-3-2019.ppt][Lesson_10.27-3-2019.ppt]]: tenth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_11.1_4_2019.ppt][Lesson_11.1_4_2019.ppt]]: eleventh lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_12.3_4_2019.ppt][Lesson_12.3_4_2019.ppt]]: twelveth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_13.17-4-2019.ppt][Lesson_13.17-4-2019.ppt]]: thirteenth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_14.29-4-2019.ppt][Lesson_14.29-4-2019.ppt]]: fourteenth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_15.6-5-2019.ppt][Lesson_15.6-5-2019.ppt]]: fiftheenth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_16.8_5_2019.ppt][Lesson_16.8_5_2019.ppt]]: sixteenth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_17.15_5_2019.ppt][Lesson_17.15_5_2019.ppt]]: seventeenth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_18.20_5_2019.ppt][Lesson_18.20_5_2019.ppt]]: eighteenth lesson a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_19-20.29_5_2019.ppt][Lesson_19-20.29_5_2019.ppt]]: nintheenth and twentieth lessons a.y. 2018/19 <p> </p> <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF1-2019.pdf][MF1-2019.pdf]]: first lecture about project a.y. 2018/19 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF2-2019.pdf][MF2-2019.pdf]]: second lecture about project a.y. 2018/19 <p> </p>
 * a.y 2017/18 * <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_1.28_2_2018.pdf][Lesson_1.28_2_2018.pdf]]: first lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_1.28_2_2018.ppt][Lesson_1.28_2_2018.ppt]]: first lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_2.7_3_2018.pdf][Lesson_2.7_3_2018.pdf]]: second lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_2.7_3_2018_.pptx][Lesson_2.7_3_2018_.pptx]]: second lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_3.12_3_2018.pdf][Lesson_3.12_3_2018.pdf]]: third lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_3.12_3_2018_.pptx][Lesson_3.12_3_2018_.pptx]]: third lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_4.14_3_2018.pdf][Lesson_4.14_3_2018.pdf]]: forth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_4.14_3_2018.pptx][Lesson_4.14_3_2018.pptx]]: forth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_5.19_3_2018.ppt][Lesson_5.19_3_2018.ppt]]: fifth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_5.19_3_2018.pdf][Lesson_5.19_3_2018.pdf]]: fifth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_6.21-3-2018.pdf][Lesson_6.21-3-2018.pdf]]: sixth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_6.21-3-2018.ppt][Lesson_6.21-3-2018.ppt]]: sixth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_7.26-3-2018.pdf][Lesson_7.26-3-2018.pdf]]: seventh lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_7.26-3-2018.ppt][Lesson_7.26-3-2018.ppt]]: seventh lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_8.28-3-2018.pdf][Lesson_8.28-3-2018.pdf]]: eighth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_8.28-3-2018.ppt][Lesson_8.28-3-2018.ppt]]: eighth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_9.4-4-2018.pdf][Lesson_9.4-4-2018.pdf]]: ninth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_9.4-4-2018.ppt][Lesson_9.4-4-2018.ppt]]: ninth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_10.9-4-2018.pdf][Lesson_10.9-4-2018.pdf]]: tenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_10.9-4-2018.ppt][Lesson_10.9-4-2018.ppt]]: tenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-11.23_4_2018.ppt][Lesson-11.23_4_2018.ppt]]: eleventh lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-11.23_4_2018.pdf][Lesson-11.23_4_2018.pdf]]: eleventh lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-12.2-5-2018.pdf][Lesson-12.2-5-2018.pdf]]: twelveth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_12.2-5-2018.ppt][Lesson_12.2-5-2018.ppt]]: twelveth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_13.7-5-2018.pdf][Lesson_13.7-5-2018.pdf]]: thirteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_13.7-5-2018.ppt][Lesson_13.7-5-2018.ppt]]: thirteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_14.9-5-2018.pdf][Lesson_14.9-5-2018.pdf]]: fourteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_14.9-5-2018.ppt][Lesson_14.9-5-2018.ppt]]: fourteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-15.16_5_2018.pdf][Lesson-15.16_5_2018.pdf]]: fifteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-15.16_5_2018.ppt][Lesson-15.16_5_2018.ppt]]: fifteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_16.21_5_2018.pdf][Lesson_16.21_5_2018.pdf]]: sixteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_16.21_5_2018.ppt][Lesson_16.21_5_2018.ppt]]: sixteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_17.23_5_2018.pdf][Lesson_17.23_5_2018.pdf]]: seventeenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_17.23_5_2018.ppt][Lesson_17.23_5_2018.ppt]]: seventeenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-18.28_5_2018.pdf][Lesson-18.28_5_2018.pdf]]: eighteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-18.28_5_2018.ppt][Lesson-18.28_5_2018.ppt]]: eighteenth lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-19.30_5_2018.pdf][Lesson-19.30_5_2018.pdf]]: ninetheen lesson a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-19.30_5_2018.ppt][Lesson-19.30_5_2018.ppt]]: ninetheen lesson a.y. 2017/18 <p> </p> <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF1.pdf][MF1.pdf]]: lectures about project a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF2.pdf][MF2.pdf]]: lectures about project a.y. 2017/18 <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF3.pdf][MF3.pdf]]: lectures about project a.y. 2017/18 <p> </p> <p> </p> <p> </p>
 * a.y 2016/17 * <p> </p>
 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_1.20_2_2017.ppt][Lesson_1.20_2_2017.ppt]]: first lesson <p> </p>
 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_2.22_2_2017_.pptx][Lesson_2.22_2_2017_.pptx]]: second lesson <p> </p>
* [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_3.27_2_2017_.pptx][Lesson_3.27_2_2017_.pptx]]: third lesson

* [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_4.1_3_2017.pptx][Lesson_4.1_3_2017.pptx]]: forth lesson

* [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_5.6_3_2017.ppt][Lesson_5.6_3_2017.ppt]]: fifth lesson

* [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_6.8-3-2017.ppt][Lesson_6.8-3-2017.ppt]]: sixth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_7.13-3-2017.ppt][Lesson_7.13-3-2017.ppt]]: seventh lesson

* [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_8.15-3-2017.ppt][Lesson_8.15-3-2017.ppt]]: eighth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_9.20-3-2017.ppt][Lesson_9.20-3-2017.ppt]]: ninth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_10.22-3-2017.ppt][Lesson_10.22-3-2017.ppt]]: tenth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/exercises_5-4-2017.ppt][exercises_5-4-2017.ppt]]: exercises on the first part

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson_11.12_4_2017.ppt][Lesson_11.12_4_2017.ppt]]: eleventh lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-12.19-4-2017.ppt][Lesson-12.19-4-2017.ppt]]: twelveth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-13.26-4-2017.ppt][Lesson-13.26-4-2017.ppt]]: thirteenth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-14.3-5-2017.ppt][Lesson-14.3-5-2017.ppt]]: fourteenth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-15.8-5-2017.ppt][Lesson-15.8-5-2017.ppt]]: fifteenth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-16.10-5-2017.ppt][Lesson-16.10-5-2017.ppt]]: sixteenth lesson

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-17.17-5-2017.ppt][Lesson-17.17-5-2017.ppt]]: seventheenth lesson

  * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/Lesson-18.22-5-2017.ppt][Lesson-18.22-5-2017.ppt]]: eighteenth lesson

  * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF1.pdf][MF1.pdf]]: first lecture about project

  * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF2.pdf][MF2.pdf]]: second lecture about project

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/MF3.pdf][MF3.pdf]]: third lecture about project

 * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/results_of__both_tests.pdf][results_of__both_tests.pdf]]: results of both tests

---++ Useful Links
   * [[http://www.uniroma1.it/][Sapienza Università di Roma]]
   * [[http://w3.uniroma1.it/dipinfo/corsi_di_studio/default.asp?iId=JKLFE][Corso di Laurea in Informatica]]
   * [[http://w3.uniroma1.it/dipinfo/][Dipartimento di Informatica]]
   * [[http://www.i3s.uniroma1.it//][Facoltà di Ingegneria dell'informazione, informatica e statistica]]
   * [[http://www.infostud.it/][Portale degli studenti di Informatica]]
   * [[http://phd.di.uniroma1.it/][Dottorato di Ricerca in Informatica]]
   * [[%SCRIPTURL{"view"}%][Homepage di TWiki]]
   * [[http://opac.uniroma1.it/][Catalogo delle biblioteche dell'università]]<hr /> <p> </p> <p> </p> <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/dens.pdf][dens.pdf]]: Notes on denotational semantics
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/appunti_semantica.pdf][appunti_semantica.pdf]]: notes (in italian) <p> </p>
   * [[http://twiki.di.uniroma1.it/pub/MFS/WebHome/intro2ccs.pdf][intro2ccs.pdf]]: notes on CCS and Hennessy Milner logic <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p> <p> </p>
</td> </tr> </tbody> </table>
This topic: MFS > WebHome
> FormalMethodsInSoftwareDevelopmentBefore2019
Topic revision: r1 - 2019-09-18 - IgorMelatti