Introduction à la spécification et vérification des systèmes

Learning objectives

(1): Building intuition
(2): Standard Concepts
(3): Advanced Topics
(X, p): Practical Application

1 Overview Testing vs. Verification
1.1 Modelling and abstracting real-world systems (1)
1.2 From systems to words, traces and languages (1)
1.3 Reduction of regular expressions to finite automata (2, p)
2 A tour through the landscape of formal methods (1)
2.1 Automata based approaches (1, 2)
2.2 Formal Proof Assistants (1)
2.3 Code analysis (1)
3 Concurrent and distributed systems
3.1 Sequential vs Concurrent execution (2)
3.2 Lamport clocks and happens-before relation (2)
3.3 Resource sharing and mutual exclusion (2, p)
3.4 Commit protocols and other distributed algorithms (3, p)
4 Design, refinement and implementation
4.1 Implementing a design (2, p)
4.2 Composition of sub-systems (3, p)