FV

Formal Verification

Objectives

This course is an introduction to the specification and verification of non-sequential algorithms, namely concurrent and distributed algorithms. After completing the course, students will be able to:

• Model a non-sequential algorithm with state machines
• Specify safety and liveness properties
• Use automatic and deductive verification tools to verify properties
• Use a proof assistant to verify simple safety properties

Program

1. Introduction to the specification and verification of non-sequential algorithms a. Modeling with state machines b. Safety and liveness properties c. Automatic and deductive verification d. Introduction to proof assistants
2. Techniques and tools for verification a. Automatic verification with TLA+ b. Deductive verification with Why3 c. The Coq proof assistant

Bibliography

• Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
• François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. The Why3 platform. Online manual.
• Yves Bertot, Pierre Castéran. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer, 2004.