Mechanical Verification Projects

• Complete assertional proof rules for progress under weak and strong fairness (2012).
• Partial mutual exclusion for infinitely many processes (2011).
• Starvation-free mutual exclusion with semaphores (2011).
• A mechanical verification of Lamport's bakery algorithm (2010), primarily to illustrate the technique.
• Revisiting mutual exclusion by Lycklama-Hadzilacos (2010).
• Bounded nonatomic mutual exclusion together with A.A. Aravind (2009).
• Eternity variables to prove simulation of specifications. This directory also contains a revised criterion for atomicity, with an application to an implementation of an atomic variable by Haldar and Vidyasankar (papers in 2004, 2005, 2007, 2008). Some of the proofs use the theorem prover NQTHM, see below.
• Simple concurrent garbage collection together with M. I. Lali (2007).
• Formalizing a hierarchical file system together with M. I. Lali (2009).
• Queue based mutual exclusion together with A.A. Aravind (2007).
• Sequential consistency of the lazy caching algorithm (two papers in 2006)
• Lock-free parallel Garbage Collection by Mark & Sweep together with Gao Hui (Groningen University) and J.F. Groote (Eindhoven University of Technology) (papers in 2005, 2007)
• A formal reduction for lock-free parallel algorithms together with Gao Hui (papers in 2004, 2007)
• Lock-free dynamic hash tables with open addressing together with Gao Hui (Groningen University) and J.F. Groote (Eindhoven University of Technology) (papers in 2004, 2005)

• NQTHM proving imperative programs (papers in 1997, 1998, 2002)
• Waitfree distributed memory management (CaRuD) together with J.F. Groote (Eindhoven University of Technology) (paper in 2001)
• A mechanical proof of the Gallager-Humblet-Spira algorithm (paper in 1999)
• The design of a linearization of a concurrent data object (paper in 1998)
• A mechanical proof of Segall's PIF algorithm (paper in 1997)

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