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.

• Type: Conference
• Year: 2001
• Where: CHARME
• Authors: Kenneth L. McMillan
• Keywords: Cache Coherence Protocol, CHARME 2001, Hardware, Proof Process, SMV Proof Assistant