Formal Methods in Software Development

teacher: Anna Labella

a.a. 2018-19

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


Lectures timetable

Time table Classroom
Mon. and Wed. 8.00-10.30 Aula 2, via del Castro Laurenziano, 7a


Notifications:

* 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

* WARNING! All the lessons will begin at 8:30am

* Lessons will start on Monday 25th of February

* There will be no lesson on Wednesday 24th of April

* There will be no lesson on Monday 13th of May

* There will be no lesson on Monday 27th of May


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)

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

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 *

* a.y 2017/18 *

  • MF1.pdf: lectures about project a.y. 2017/18

  • MF2.pdf: lectures about project a.y. 2017/18

  • MF3.pdf: lectures about project a.y. 2017/18

* a.y 2016/17 *

* Lesson_1.20_2_2017.ppt: first lesson

* Lesson_2.22_2_2017_.pptx: second lesson

* Lesson_3.27_2_2017_.pptx: third lesson

* Lesson_4.1_3_2017.pptx: forth lesson

* Lesson_5.6_3_2017.ppt: fifth lesson

* Lesson_6.8-3-2017.ppt: sixth lesson

* Lesson_7.13-3-2017.ppt: seventh lesson

* Lesson_8.15-3-2017.ppt: eighth lesson

* Lesson_9.20-3-2017.ppt: ninth lesson

* Lesson_10.22-3-2017.ppt: tenth lesson

* exercises_5-4-2017.ppt: exercises on the first part

* Lesson_11.12_4_2017.ppt: eleventh lesson

* Lesson-12.19-4-2017.ppt: twelveth lesson

* Lesson-13.26-4-2017.ppt: thirteenth lesson

* Lesson-14.3-5-2017.ppt: fourteenth lesson

* Lesson-15.8-5-2017.ppt: fifteenth lesson

* Lesson-16.10-5-2017.ppt: sixteenth lesson

* Lesson-17.17-5-2017.ppt: seventheenth lesson

* Lesson-18.22-5-2017.ppt: eighteenth lesson

* MF1.pdf: first lecture about project

* MF2.pdf: second lecture about project

* MF3.pdf: third lecture about project

* results_of__both_tests.pdf: results of both tests

Useful Links

Topic attachments
I Attachment History Action Size Date Who Comment
PDFpdf Lesson-11.23_4_2018.pdf r1 manage 3047.8 K 2018-04-27 - 08:53 AnnaLabella eleventh lesson
PowerPointppt Lesson-11.23_4_2018.ppt r1 manage 1865.5 K 2018-04-27 - 08:53 AnnaLabella eleventh lesson
PowerPointppt Lesson-12.19-4-2017.ppt r1 manage 569.0 K 2017-04-19 - 16:05 AnnaLabella twelveth lesson
PDFpdf Lesson-12.2-5-2018.pdf r1 manage 1525.9 K 2018-05-04 - 09:04 AnnaLabella Twelveth lesson
PDFpdf Lesson-12.30-4-2018.pdf r1 manage 1525.9 K 2018-05-04 - 06:57 AnnaLabella Twelveth lesson
PowerPointppt Lesson-12.30-4-2018.ppt r1 manage 603.5 K 2018-05-04 - 06:57 AnnaLabella Twelveth lesson
PowerPointppt Lesson-13.26-4-2017.ppt r1 manage 1631.0 K 2017-04-26 - 16:43 AnnaLabella thirteenth lesson
PowerPointppt Lesson-14.3-5-2017.ppt r1 manage 482.0 K 2017-05-03 - 08:56 AnnaLabella fourteenth lesson
PDFpdf Lesson-15.16_5_2018.pdf r1 manage 2096.2 K 2018-05-16 - 14:38 AnnaLabella fiftheenth lesson
PowerPointppt Lesson-15.16_5_2018.ppt r1 manage 1250.5 K 2018-05-16 - 14:38 AnnaLabella fiftheenth lesson
PowerPointppt Lesson-15.8-5-2017.ppt r2 r1 manage 1622.0 K 2017-05-09 - 09:06 AnnaLabella fifteenth lesson
PowerPointppt Lesson-16.10-5-2017.ppt r1 manage 2348.0 K 2017-05-10 - 09:16 AnnaLabella sixteenth lesson
PowerPointppt Lesson-17.17-5-2017.ppt r1 manage 833.5 K 2017-05-17 - 10:16 AnnaLabella seventheeth
PowerPointppt Lesson-18.22-5-2017.ppt r1 manage 554.0 K 2017-05-22 - 09:03 AnnaLabella eighteenth lesson
PDFpdf Lesson-18.28_5_2018.pdf r2 r1 manage 2976.0 K 2018-05-30 - 13:44 AnnaLabella eighteenth lesson a.y. 2017/18
PowerPointppt Lesson-18.28_5_2018.ppt r2 r1 manage 813.0 K 2018-05-30 - 13:44 AnnaLabella eighteenth lesson a.y. 2017/18
PDFpdf Lesson-19.30_5_2018.pdf r1 manage 966.3 K 2018-05-30 - 13:46 AnnaLabella ninetheen lesson a.y. 2017/18
PowerPointppt Lesson-19.30_5_2018.ppt r1 manage 339.5 K 2018-05-30 - 13:46 AnnaLabella ninetheen lesson a.y. 2017/18
PowerPointppt Lesson_1.20_2_2017.ppt r1 manage 551.5 K 2017-02-21 - 07:16 AnnaLabella first lesson
PowerPointppt Lesson_1.25_2_2019.ppt r1 manage 630.0 K 2019-02-27 - 13:59 AnnaLabella first lesson a.y. 2018/19
PDFpdf Lesson_1.28_2_2018.pdf r1 manage 3011.5 K 2018-03-22 - 07:56 AnnaLabella  
PowerPointppt Lesson_1.28_2_2018.ppt r1 manage 598.5 K 2018-03-22 - 07:56 AnnaLabella  
PowerPointppt Lesson_10.22-3-2017.ppt r1 manage 2037.0 K 2017-03-23 - 11:59 AnnaLabella tenth lesson
PowerPointppt Lesson_10.27-3-2019.ppt r1 manage 755.5 K 2019-03-28 - 12:09 AnnaLabella tenth lesson a.y. 2018/19
PDFpdf Lesson_10.9-4-2018.pdf r1 manage 2871.6 K 2018-04-10 - 10:06 AnnaLabella tenth lesson a.y. 2017/18
PowerPointppt Lesson_10.9-4-2018.ppt r1 manage 1975.5 K 2018-04-10 - 10:06 AnnaLabella tenth lesson a.y. 2017/18
PowerPointppt Lesson_11.12_4_2017.ppt r1 manage 2596.5 K 2017-04-14 - 09:02 AnnaLabella eleventh lesson
PowerPointppt Lesson_11.1_4_2019.ppt r1 manage 1321.0 K 2019-04-03 - 16:55 AnnaLabella eleventh lesson a.y. 2018/19
PowerPointppt Lesson_12.2-5-2018.ppt r1 manage 603.5 K 2018-05-06 - 09:17 AnnaLabella twelveth lesson
PowerPointppt Lesson_12.3_4_2019.ppt r1 manage 1946.5 K 2019-04-03 - 16:57 AnnaLabella twelveth lesson a.y. 2018/19
PowerPointppt Lesson_13.17-4-2019.ppt r1 manage 715.0 K 2019-04-18 - 07:09 AnnaLabella thirteenth lesson a.y. 2018/19
PDFpdf Lesson_13.7-5-2018.pdf r1 manage 3311.6 K 2018-05-10 - 08:56 AnnaLabella thirteen lesson 7_5_2018
PowerPointppt Lesson_13.7-5-2018.ppt r1 manage 1667.0 K 2018-05-10 - 08:56 AnnaLabella thirteen lesson 7_5_2018
PowerPointppt Lesson_14.29-4-2019.ppt r1 manage 866.0 K 2019-05-08 - 14:57 AnnaLabella fourteenth lesson a.y. 2018/19
PDFpdf Lesson_14.9-5-2018.pdf r1 manage 1916.4 K 2018-05-10 - 08:56 AnnaLabella thirteen lesson 7_5_2018
PowerPointppt Lesson_14.9-5-2018.ppt r1 manage 561.5 K 2018-05-10 - 08:56 AnnaLabella thirteen lesson 7_5_2018
PowerPointppt Lesson_15.6-5-2019.ppt r1 manage 1101.5 K 2019-05-08 - 14:58 AnnaLabella fiftheenth lesson a.y. 2018/19
PDFpdf Lesson_16.21_5_2018.pdf r1 manage 2229.0 K 2018-05-24 - 14:32 AnnaLabella seventeenth lesson a.y. 2017/18
PowerPointppt Lesson_16.21_5_2018.ppt r1 manage 2096.5 K 2018-05-24 - 14:24 AnnaLabella sixteenth lesson a.y. 2017/18
PowerPointppt Lesson_16.8_5_2019.ppt r1 manage 1314.5 K 2019-05-08 - 14:59 AnnaLabella sixteenth lesson a.y. 2018/19
PowerPointppt Lesson_17.15_5_2019.ppt r1 manage 1972.5 K 2019-05-16 - 07:27 AnnaLabella seventith lesson a.y. 2018/19
PDFpdf Lesson_17.23_5_2018.pdf r1 manage 2551.8 K 2018-05-24 - 14:32 AnnaLabella seventeenth lesson a.y. 2017/18
PowerPointppt Lesson_17.23_5_2018.ppt r1 manage 1063.0 K 2018-05-24 - 14:24 AnnaLabella sixteenth lesson a.y. 2017/18
PowerPointppt Lesson_18.20_5_2019.ppt r1 manage 1059.5 K 2019-05-29 - 14:19 AnnaLabella eighteenth lesson a.y. 2018/19
PowerPointppt Lesson_19-20.29_5_2019.ppt r1 manage 1026.0 K 2019-05-29 - 14:15 AnnaLabella nintheenth and twentieth lessons
PowerPointpptx Lesson_2.22_2_2017_.pptx r1 manage 211.9 K 2017-02-23 - 11:34 AnnaLabella second lesson
PowerPointpptx Lesson_2.27_2_2019_.pptx r1 manage 417.7 K 2019-02-27 - 14:01 AnnaLabella second lesson a.y. 2018/19
PDFpdf Lesson_2.7_3_2018.pdf r1 manage 2714.8 K 2018-03-22 - 07:56 AnnaLabella  
PowerPointpptx Lesson_2.7_3_2018_.pptx r1 manage 417.6 K 2018-03-07 - 15:05 AnnaLabella second lesson a.y. 2017/18
PDFpdf Lesson_3.12_3_2018.pdf r1 manage 3089.8 K 2018-03-22 - 07:57 AnnaLabella  
PowerPointpptx Lesson_3.12_3_2018_.pptx r1 manage 514.9 K 2018-03-12 - 16:37 AnnaLabella third lesson_12_3_2018
PowerPointpptx Lesson_3.27_2_2017_.pptx r1 manage 427.8 K 2017-02-27 - 16:30 AnnaLabella third lesson
PowerPointpptx Lesson_3.4_3_2019_.pptx r1 manage 513.6 K 2019-03-07 - 07:17 AnnaLabella third lesson a.y. 2018/2019
PDFpdf Lesson_4.14_3_2018.pdf r1 manage 2543.4 K 2018-03-22 - 07:57 AnnaLabella  
PowerPointpptx Lesson_4.14_3_2018.pptx r1 manage 392.0 K 2018-03-14 - 16:18 AnnaLabella forth lesson a.y. 2017/18
PowerPointpptx Lesson_4.1_3_2017.pptx r1 manage 283.3 K 2017-03-07 - 08:32 AnnaLabella forth lesson
PowerPointpptx Lesson_4.6_3_2019.pptx r1 manage 363.6 K 2019-03-07 - 07:18 AnnaLabella fourth lesson a.y. 2018/2019
PowerPointppt Lesson_5.11_3_2019.ppt r1 manage 1451.5 K 2019-03-13 - 14:41 AnnaLabella fifth lesson a.y. 2018/19
PDFpdf Lesson_5.19_3_2018.pdf r1 manage 3745.6 K 2018-03-22 - 08:03 AnnaLabella  
PowerPointppt Lesson_5.19_3_2018.ppt r1 manage 1448.5 K 2018-03-20 - 07:55 AnnaLabella fifth lesson a.y. 2017/18
PowerPointppt Lesson_5.6_3_2017.ppt r1 manage 865.5 K 2017-03-07 - 08:33 AnnaLabella fifth lesson
PowerPointppt Lesson_6.13-3-2019.ppt r1 manage 767.0 K 2019-03-13 - 14:42 AnnaLabella sixth lesson a.y. 2018/19
PDFpdf Lesson_6.21-3-2018.pdf r1 manage 2137.7 K 2018-03-22 - 08:03 AnnaLabella  
PowerPointppt Lesson_6.21-3-2018.ppt r1 manage 766.5 K 2018-03-22 - 08:03 AnnaLabella  
PowerPointppt Lesson_6.8-3-2017.ppt r1 manage 774.5 K 2017-03-13 - 09:58 AnnaLabella sixth lesson
PowerPointppt Lesson_7.13-3-2017.ppt r1 manage 630.5 K 2017-03-13 - 09:57 AnnaLabella seventh lesson
PowerPointppt Lesson_7.18-3-2019.ppt r1 manage 861.0 K 2019-04-03 - 17:01 AnnaLabella seventh lesson a.y. 2018/19
PDFpdf Lesson_7.26-3-2018.pdf r1 manage 2444.9 K 2018-03-27 - 07:12 AnnaLabella seventh lesson a.y. 2017/18
PowerPointppt Lesson_7.26-3-2018.ppt r1 manage 857.0 K 2018-03-27 - 07:12 AnnaLabella seventh lesson a.y. 2017/18
PowerPointppt Lesson_8.15-3-2017.ppt r1 manage 721.0 K 2017-03-16 - 09:45 AnnaLabella eighth lesson
PowerPointppt Lesson_8.20-3-2018.ppt r1 manage 717.0 K 2019-03-20 - 14:15 AnnaLabella eighth lesson a.y. 2018/19
PDFpdf Lesson_8.28-3-2018.pdf r1 manage 2101.2 K 2018-04-04 - 15:05 AnnaLabella eighth lesson
PowerPointppt Lesson_8.28-3-2018.ppt r1 manage 710.0 K 2018-04-04 - 15:05 AnnaLabella eighth lesson
PowerPointppt Lesson_9.20-3-2017.ppt r1 manage 1163.5 K 2017-03-20 - 17:41 AnnaLabella ninth lesson
PowerPointppt Lesson_9.25-3-2019.ppt r1 manage 985.0 K 2019-03-28 - 12:05 AnnaLabella tenth lesson a.y. 2018/19
PDFpdf Lesson_9.4-4-2018.pdf r1 manage 2976.7 K 2018-04-04 - 15:07 AnnaLabella ninth lesson
PowerPointppt Lesson_9.4-4-2018.ppt r1 manage 1465.0 K 2018-04-04 - 15:07 AnnaLabella ninth lesson
PDFpdf MF1-2019.pdf r1 manage 719.7 K 2019-04-13 - 10:41 AnnaLabella first lecture about project a.y. 2018/19
PDFpdf MF1.pdf r2 r1 manage 726.7 K 2018-05-06 - 09:16 AnnaLabella lectures about project
PDFpdf MF2-2019.pdf r1 manage 400.3 K 2019-04-13 - 10:42 AnnaLabella second lecture about project a.y. 2018/19
PDFpdf MF2.pdf r2 r1 manage 657.6 K 2018-05-06 - 09:16 AnnaLabella lectures about project
PDFpdf MF3.pdf r2 r1 manage 551.2 K 2018-05-06 - 09:16 AnnaLabella lectures about project
PDFpdf appunti_semantica.pdf r1 manage 3039.1 K 2014-05-02 - 06:38 AnnaLabella dispense
PDFpdf dens.pdf r1 manage 340.2 K 2018-05-04 - 06:59 AnnaLabella Notes on denotational semantics
PowerPointppt exercises_5-4-2017.ppt r1 manage 325.5 K 2017-04-09 - 09:47 AnnaLabella exercises on the first part
PDFpdf intro2ccs.pdf r1 manage 504.5 K 2017-05-10 - 09:20 AnnaLabella notes on CCS and Hennessy Milner logic
PDFpdf results_of__both_tests.pdf r1 manage 19.7 K 2017-05-24 - 16:54 AnnaLabella results of both tests
Edit | Attach | Watch | Print version | History: r118 < r117 < r116 < r115 < r114 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r118 - 2019-06-24 - AnnaLabella





 
ATTENZIONE: per lavori ACEA sulla cabina elettrica il server resterą spento
nei giorni 19-22 agosto.
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2019 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback