Mechanical Verification Projects
The following projects have been performed with the proof assistant
In particular, 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: Saturday 27 July, 2013
Back to my home page.
Wim H. Hesselink