This project was done to illustrate the technique. Slides are available. The algorithm has been extended to allow infinitely many processes using concurrently extendable arrays. The PVS specification consists of two files, one for safety and one for liveness. This is proved in a PVS dump file, which can be inspected with PVS (version 5.0).
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink