In the paper
Murali Talupur and Mark Tuttle.
Going with the flow:
Parameterized verification using message flows. In Proceedings of the
8th International Conference on Formal
Methods in Computer-Aided Design (FMCAD), November 2008.
we used the following murphi models as our examples (grab
them all as a single file)
- The Flash and German
cache coherence protocols as modeled by Ching-Tsun Chou and used in the
paper C.-T. Chou, P. K. Mannava, and S. Park, A simple method for
parameterized verification of cache coherence protocols, FMCAD 2004.
- The Flash and
German protocols abstracted with flows as described in our paper.