Mechanical Verification Projects
The following projects have been performed with the proof assistant
More specifically, several projects about mutual exclusion in shared memory:
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.
Last modified: Sat May 2 14:00:14 CEST 2020
Back to my home page.