Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
by Henri Debrat and Stephan Merz
Stephan Merz
2012
2011
A Definitional Encoding of TLA* in Isabelle/HOL
by Gudmund Grov and Stephan Merz
2005
Proving the Correctness of Disk Paxos
by Mauro Jaskelioff and Stephan Merz