This class is about formal design of software using model-checking. Model-checking is a formal method that consists in building a model of the system under study, then in automatically proving the correctness of the model. This class focuses on modeling, formal specifications in Linear Temporal Logic (LTL), and model-checking algorithms. It combines theoretical aspects as well as practical applications with TLA+.

Lectures

• Introduction
  • Further reading:
    • How Amazon Web Services Uses Formal Methods (2015)
    • Systems Correctness Practices at AWS (2025)
  • Test vs. model-checking vs. proof
• Semantics modelling of systems
  • Modelling programs
• Introduction to formal verification
  • Formal design of a distributed mutual exclusion protocol
• Temporal specifications
  • Further reading: Safety, Liveness and Fairness sections 1 and 2
  • Formal modeling and verification of Peterson’s algorithm - Part 1
• Fairness for liveness verification
  • Formal modeling and verification of Peterson’s algorithm - Part 2
• Algorithmic verification
• Model-checking under fairness assumptions