Checking Cache-Coherence Protocols with TLA+

  • Rajeev Joshi
  • 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].