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
• Test vs. model-checking vs. proof
• Semantics modelling of systems
• Modelling programs
• Debugging a Java multi-threaded program
• Formal specification and verification
  • mutex_lock_skeleton.tla
  • Further reading: Safety, Liveness and Fairness sections 1 and 2
• Fairness for liveness verification
• Model-checking under fairness assumptions