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.
Last modified: 25 August, 2016