Memoir—Formal Specs and Correctness Proofs

MSR-TR-2011-19 |


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.