Understand the foundations and apply the automatic tools for program correctness, and specially with respect to temporal logic properties.
System Verification 1
Modelling Concurrent Systems 19
Linear-Time Properties 89
Regular Properties 151
Linear Temporal Logic 229
Computation Tree Logic 313
Timed Automata 673
67% Spoken exam (open book) including exercises
33% project evaluation
Main reference book: Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, The MIT Press (May 31, 2008).
Principles of the Spin Model Checker by M. Ben-Ari
The SPIN Model Checker: Primer and Reference by Gerard J. Holzmann
Systems and Software Verification: Model-Checking Techniques and Tools by B. Berard, M. Bidoit, A. Finkel, and F. Laroussinie
Model Checking by E. M. Clarke et al.
| Training | Study programme | Block | Credits | Mandatory |
|---|---|---|---|---|
| Standard | 0 | 5 | ||
| Standard | 0 | 5 | ||
| Standard | 0 | 5 | ||
| Standard | 1 | 5 | ||
| Standard | 2 | 5 | ||
| Standard | 2 | 5 |