Mechanized proofs for the Parameter Abstraction and Guard Strengthening Principle in Parameterized Verification of Cache Coherence Protocols

被引：0

作者：

Li, Yongjian ^{[1
]}

机构：

[1] CAS, Inst Software, Comp Sci Lab, Beijing, Peoples R China

来源：

APPLIED COMPUTING 2007, VOL 1 AND 2 | 2007年

关键词：

Parameterized verification; Theorem proving; Symmetry;

D O I：

暂无

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

Chou, Mannava, and Park proposed a novel method for verification of safety proper-ties of cache protocols, which is underpinned by the principle of parameter abstraction and guard strengthening. However, no one has formally proved the correctness of this method itself. In this work, we want to fill the gap in the literature. We believe that our work provides an alternative to formally justify this method. The key points of our theory are symmetry and the introduction of an intermediate guard strengthening protocol. We mechanize our theory in Isabelle/HOL.

引用

页码：1534 / 1535

页数：2