Model checking [INFOM471]
- 5 credits
- 30h+15h
- 1st quarter
Language of instruction: French / FrançaisTeacher: Schobbens Pierre
Learning outcomes
Understand the foundations and apply the automatic tools for program correctness, and specially with respect to temporal logic properties.
Table of contents
-
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
Teaching methods
Course of lectures ex-cathedra;
Exercices ;
From 2017, the project will be done with support of the SCADE tool by ANSYS, and perhaps the UPPAAL tool.
Evaluations
67% Spoken exam (open book) including exercises
33% project evaluation
Recommended readings
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.
Language of instruction
French / FrançaisLocation for course
NAMUROrganizer
Faculté d'informatiquerue Grandgagnage 21
5000 NAMUR
P. 081725252
F. 081724967
secretariat.info@unamur.be
