SWENG @ Télécom Paris

Formal Methods

Edition: 2026/2027 (1st ed.)
Last-Modified: 2025-06-30

Teachers

  • Rabéa Ameur-Boulifa, contact: email

Syllabus

This course covers the use of formal methods to design safe and reliable software. It explores specification, verification, and proof techniques to ensure system correctness and robustness.

By the end of the course, students will be able to:

  • Understand the foundations of formal methods in software engineering
  • Model software using formal languages
  • Verify program correctness through formal proofs
  • Use verification and model-checking tools
  • Apply formal methods to real-world cases

Here are some key topics covered in the course:

  • Introduction to Formal Methods – Importance and applications in software development.
  • Mathematical Foundations – Logic, set theory, and automata theory.
  • Specification Languages – B-Method.
  • Model Checking – Verifying system properties automatically.
  • Program Verification – Ensuring software correctness using the B Method to prove compliance with specifications..
  • Formal Verification of Critical Systems – Case studies in real-life domain.
  • Refinement and Correct-by-Construction Development – Transforming specifications into verified code.
  • Tool Support for Formal Methods – Program Verification – Learning to use a formal verification tool, specifically Atelier B, to ensure software correctness.