Sciweavers

CHARME
2001
Springer

Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking

14 years 1 months ago
Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking
We consider the formal verification of the cache coherence protocol of the Stanford FLASH multiprocessor for N processors. The proof uses the SMV proof assistant, a proof system based on symbolic model checking. The proof process is described step by step. The protocol model is derived from an earlier proof of the FLASH protocol, using the PVS system, allowing a direct comparison between the two methods.
Kenneth L. McMillan
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2001
Where CHARME
Authors Kenneth L. McMillan
Comments (0)