|
1-Dec-15
|
Activities
|
Organizer(s)
|
| 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 |
|
2-Dec-15
|
Activities
|
Organizer(s)
|
| 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. |