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
相关论文
共 26 条
  • [1] Efficient Verification of Parameterized Cache Coherence Protocols
    Qu, WanXia
    Guo, Yang
    Pang, ZhengBin
    Yang, XiaoDong
    [J]. PROCEEDINGS OF THE 9TH INTERNATIONAL CONFERENCE FOR YOUNG COMPUTER SCIENTISTS, VOLS 1-5, 2008, : 154 - 159
  • [2] A Novel Approach to Parameterized Verification of Cache Coherence Protocols
    Li, Yongjian
    Duan, Kaiqiang
    Lv, Yi
    Pang, Jun
    Cai, Shaowei
    [J]. PROCEEDINGS OF THE 34TH IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD), 2016, : 560 - 567
  • [3] A simple method for parameterized verification of cache coherence Protocols
    Chou, CT
    Mannava, PK
    Park, S
    [J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2004, 3312 : 382 - 398
  • [4] A simple method for parameterized verification of cache coherence protocols
    Chou, CT
    Mannava, PK
    Park, S
    [J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2004, 3312 : 382 - 398
  • [5] Exact and efficient verification of parameterized cache coherence protocols
    Emerson, EA
    Kahlon, V
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 247 - 262
  • [6] Constraint-based verification of parameterized cache coherence Protocols
    Delzanno, G
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2003, 23 (03) : 257 - 301
  • [7] Constraint-Based Verification of Parameterized Cache Coherence Protocols
    Giorgio Delzanno
    [J]. Formal Methods in System Design, 2003, 23 : 257 - 301
  • [8] Verification techniques for cache coherence protocols
    Pong, F
    Dubois, M
    [J]. ACM COMPUTING SURVEYS, 1997, 29 (01) : 82 - 126
  • [9] An Automatic Parameterized Verification of FLASH Cache Coherence Protocol
    Li, Yongjian
    Cao, Jialun
    Duan, Kaiqiang
    [J]. 2018 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS 2018), 2018, : 47 - 58
  • [10] A NEW APPROACH FOR THE VERIFICATION OF CACHE COHERENCE PROTOCOLS
    PONG, F
    DUBOIS, M
    [J]. IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 1995, 6 (08) : 773 - 787
123