Mechanical Verification Projects

The following projects have been performed with the proof assistant PVS. More specifically, several projects about mutual exclusion in shared memory: Older work: The following projects have been done with the theorem prover NQTHM of Boyer and Moore.

My former PhD student Gao Hui defended his thesis "Design and Verification of Lock-free Parallel Algorithms" successfully in Groningen on 15 April 2005.

Short introduction to theorem proving with PVS

Comments and questions are welcome.
Back to my home page.

Last modified: Sat Sep 23 13:44:58 CEST 2023