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: Tue Apr 16 20:49:55 CEST 2024