Abstract:We present a new method for computing invariants for cache coherence protocol in this paper. The verification of cache coherence protocols is always a challenge as we have to check the safety properties of cache coherence protocol with arbitrary nodes. By searching the relations between the invariants and the rules of cache coherence protocol, we can verify the cache coherence protocol with circular reasoning. Besides, we implement a tool to help us computing invariants for cache coherence protocol. We also have experiments on how to apply our method to the German protocol with both control property and data property.