Contribution: MutualExclusion

A certification of Peterson's algorithm for managing mutual exclusion

Authors

Description

This is a proof of certification of Peterson's algorithm for managing mutual exclusion. The case of two processes is treated in the directory called ``binary'' (see the README file in this directory). The case of n processes will be available soon.

Keywords

mutual exclusion, concurrency, peterson's algorithm, co inductive types, co induction

Available files