Mechanical Verification Projects

• Waitfree linearization of an arbitrary data object (2024).
• Barriers and partial barriers (2023).
• Büchi machines (2021).
• Extensions of UNITY logic (2012 and 2020).
• Distributed resource allocation for unboundedly many processes (2012).
• Partial mutual exclusion for infinitely many processes (2011).
• Formalizing a hierarchical file system together with M. I. Lali (2009).
• Simple concurrent garbage collection together with M. I. Lali (2007).

• Verification of hardware locks (2021)
• FCFS: first-come first-served (2020)
• A software implementation of trylock, with applications in the Rectangle algorithm and Access Selection (2020). With Peter A. Buhr and Dave Dice.
• Elevator algorithms for high-contention mutual exclusion (2017), with Peter A. Buhr and Dave Dice.
• Fast mutual exclusion by the Triangle Algorithm (2014), together with Peter A. Buhr and Dave Dice.
• Tournaments for Mutual Exclusion (2016).
• Mutual exclusion by Lycklama-Hadzilacos, and Aravind (2013).
• Starvation-free mutual exclusion with semaphores (2011).
• Bakery Algorithms. This contains Lamport's Bakery Algorithm, verified in 2010, primarily to illustrate the technique. In 2015, it was supplemented with Taubenfeld's Black-White Bakery Algorithm. In 2016, I added work done with Alex Aravind on a Bakery algorithm with wrap-around tickets, with an extension to group mutual exclusion. In 2020, a variation of Taubenfeld's Black-White Bakery algorithm was developed, with a more natural encoding and simpler await conditions.
• Bounded nonatomic mutual exclusion together with A.A. Aravind (2009).
• Queue based mutual exclusion together with A.A. Aravind (2007).
• Group mutual exclusion together with A.A. Aravind (2015).

• 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.
• 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.