Tags:
create new tag
view all tags

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 *

* 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

Edit | Attach | Watch | Print version | History: r1 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r1 - 2019-09-18 - IgorMelatti

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