Abstract
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.
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Cite
CITATION STYLE
McMillan, K. L. (2001). Parameterized verification of the FLASH cache coherence protocol by compositional model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2144, pp. 179–195). Springer Verlag. https://doi.org/10.1007/3-540-44798-9_17
Readers over time
Readers' Seniority
Readers' Discipline
