Learning outcomes

Understand the foundations and apply the automatic tools for program correctness, and specially with respect to temporal logic properties.

Table of contents

  1. System Verification 1

  2. Modelling Concurrent Systems 19

  3.   Linear-Time Properties 89

  4. Regular Properties 151

  5. Linear Temporal Logic 229

  6. Computation Tree Logic 313

  7. Timed Automata 673

 

Assessment method

67% Spoken exam (open book) including exercises 

33% project evaluation

Sources, references and any support material

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

Français