Mechanical Verification Projects

The following projects have been performed with the proof assistant PVS. In particular, 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.
Wim H. Hesselink

Last modified: Saturday 27 July, 2013