paraVerifier: An automatic framework for proving parameterized cache coherence protocols

Parameterized verification of cache coherence protocols is an important but challenging research problem. We present in this paper our automatic framework paraVerifier to handle this problem: (1) it first discovers auxiliary invariants and thecorresponding causal relations between invariants and protocol rules from a small reference instance of the verified protocol; (2) the discovered invariants and causal relations can then be generalized into their parameterized form to automatically construct a formal proof to establish the correctness of the protocol. paraVerifier has been successfully applied to a number of benchmarks.