@techreport{douceur2011memoir,
author = {Douceur, John (JD) and Lorch, Jay and Parno, Bryan and Mickens, James and McCune, Jonathan M.},
title = {Memoir—Formal Specs and Correctness Proofs},
year = {2011},
month = {February},
abstract = {This tech report presents formal specifications for the Memoir system and proofs of the system's correctness. The proofs were constructed manually but have been programmatically machine-verified using the TLA+ Proof System. Taken together, the specifications and proofs contain 61 top-level definitions, 182 LET-IN definitions, 74 named theorems, and 5816 discrete proof steps. The proofs address only the safety of the Memoir system, not the liveness of the system. Safety is proven by showing that a formal low-level specification of the Memoir-Basic system implements a formal high-level specification of desired behavior. The proofs then show that a formal specification of the Memoir-Opt system implements the Memoir-Basic system.},
publisher = {Microsoft Research},
url = {http://approjects.co.za/?big=en-us/research/publication/memoir-formal-specs-and-correctness-proofs/},
number = {MSR-TR-2011-19},
}