Proof-checking protocols using bisimulations

被引：0
|
作者：
Röckl, C [1 ]
Esparza, J [1 ]
机构：
[1] Tech Univ Munich, Fak Informat, D-80290 Munich, Germany
来源：
CONCUR'99: CONCURRENCY THEORY | 1999年 / 1664卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We report on our experience in using the Isabelle/HOL theorem prover to mechanize proofs of observation equivalence for systems with infinitely many states, and for parameterized systems. We follow the direct approach: An infinite relation containing the pair of systems to be shown equivalent is defined, and then proved to be a weak bisimulation. The weak bisimilarity proof is split into many cases, corresponding to the derivatives of the pairs in the relation. Isabelle/HOL automatically proves simple cases, and guarantees that no case is forgotten. The strengths and weaknesses of the approach are discussed.
引用
收藏
页码：525 / 540
页数：16
相关论文
共 50 条
  • [21] SMT proof checking using a logical framework
    Aaron Stump
    Duckki Oe
    Andrew Reynolds
    Liana Hadarean
    Cesare Tinelli
    Formal Methods in System Design, 2013, 42 : 91 - 118
  • [22] Symbolic Model Checking Commitment Protocols Using Reduction
    El-Menshawy, Mohamed
    Bentahar, Jamal
    Dssouli, Rachida
    DECLARATIVE AGENT LANGUAGES AND TECHNOLOGIES VIII (DALT), 2011, 6619 : 185 - 203
  • [23] Model checking security protocols using a logic of belief
    Benerecetti, M
    Giunchiglia, F
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2000, 1785 : 519 - 534
  • [24] Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols
    Bolignano, D
    COMPUTER AIDED VERIFICATION, 1998, 1427 : 77 - 87
  • [25] An integration of model checking with automated proof checking
    Rajan, S
    Shankar, N
    Srivas, MK
    COMPUTER AIDED VERIFICATION, 1995, 939 : 84 - 97
  • [26] Towards Combining Model Checking and Proof Checking
    Jiang, Ying
    Liu, Jian
    Dowek, Gilles
    Ji, Kailiang
    COMPUTER JOURNAL, 2019, 62 (09): : 1365 - 1402
  • [27] Efficient Verification of Distributed Protocols Using Stateful Model Checking
    Saissi, Habib
    Bokor, Peter
    Muftuoglu, Can Arda
    Suri, Neeraj
    Serafini, Marco
    2013 IEEE 32ND INTERNATIONAL SYMPOSIUM ON RELIABLE DISTRIBUTED SYSTEMS (SRDS 2013), 2013, : 133 - 142
  • [28] Automated Analysis of Commitment Protocols Using Probabilistic Model Checking
    Gunay, Akin
    Song Songzheng
    Liu, Yang
    Zhang, Jie
    PROCEEDINGS OF THE TWENTY-NINTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2015, : 2060 - 2066
  • [29] Checking Software Component Behavior Using Behavior Protocols and Spin
    Kofron, Jan
    APPLIED COMPUTING 2007, VOL 1 AND 2, 2007, : 1513 - 1517
  • [30] Equivalence Checking of Quantum Protocols
    Ardeshir-Larijani, Ebrahim
    Gay, Simon J.
    Nagarajan, Rajagopal
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 478 - 492
12345