Checking Cache-Coherence Protocols with TLA+

Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark Tuttle, Yuan Yu

Journal of Formal Methods in System Design | , Vol 22: pp. 125-131

Yet another report on the TLA+ verification activity at Compaq. It mentions some work that’s been done since we wrote [140].