Formal Verification

This course is part of our Master’s specialization on formal methods and focus on the formal verification of concurrent and distributed algorithms, using both model checking with TLA+/TLC and deductive verification with Why3 and Rocq.

The current edition can be accessed here.