07.30-08.00 Registration Committee
08.30-08.45 Opening speech Head of Dept.
08.45-10.15 Introduction to Formal Verification Alessandro Abate
10.15-10.30 Coffee Break Consumption Sect.
10.30-12.00 Models: LTS and extensions; Properties: Linear-time, LTL, CTL Alessandro Abate
12.00-13.00 Ishoma Consumption Sect.
13.00-14.30 Model checking algorithms Alessandro Abate
14.30-14.45 Coffee Break Consumption Sect.
14.45-16.15 Demo of SPIN/NuSMV, exercises for the day D. Adzkiya, A. Abate
08.30-10.00 Equivalences and abstractions Alessandro Abate
10.00-10.15 Coffee Break Consumption Sect.
10.15-11.45 Formal verification and synthesis of stochastic models (and SHS) Alessandro Abate
11.45-12.45 Ishoma Consumption Sect.
12.45-14.15 Formal verification and synthesis of MPL models Dieky Adzkiya
14.15-14.30 Coffee Break Consumption Sect.
14.30-16.00 Demo of VeriSiMPL/FAUST2, exercises for the day D. Adzkiya, A. Abate
16.00-16.15 Closing ceremony Vice chair of Dept.