Heuristic search for equivalence checking

被引：0
|
作者：
Nicoletta De Francesco
Giuseppe Lettieri
Antonella Santone
Gigliola Vaglini
机构：
[1] University of Pisa,Dipartimento di Ingegneria dell’Informazione
[2] University of Sannio,Dipartimento di Ingegneria
来源：
Software & Systems Modeling | 2016年 / 15卷
关键词：
Heuristic search algorithms; Bisimulation; Concurrent systems; Model checking;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
Equivalence checking plays a crucial role in formal verification since it is a natural relation for expressing the matching of a system implementation against its specification. In this paper, we present an efficient procedure, based on heuristic search, for checking well-known bisimulation equivalences for concurrent systems specified through process algebras. The method tries to improve, with respect to other solutions, both the memory occupation and the time required for proving the equivalence of systems. A prototype has been developed to evaluate the approach on several examples of concurrent system specifications.
引用
收藏
页码：513 / 530
页数：17
相关论文
共 50 条
  • [41] Equivalence checking using abstract BDDs
    Jha, S
    Lu, Y
    Minea, M
    Clarke, EM
    INTERNATIONAL CONFERENCE ON COMPUTER DESIGN - VLSI IN COMPUTERS AND PROCESSORS, PROCEEDINGS, 1997, : 332 - 337
  • [42] Sequential equivalence checking using cuts
    Huang, Wei
    Tang, PuShan
    Ding, Min
    ASP-DAC 2005: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2005, : 455 - 458
  • [43] Arithmetic Operand Ordering for Equivalence Checking
    Weng, Yanling
    Ge, Haitong
    Yan, Xiaolang
    Kun, Ren
    Tsinghua Science and Technology, 2007, 12 (SUPPL. 1): : 235 - 239
  • [44] Semantic Equivalence Checking for HHVM Bytecode
    Benton, Nick
    PPDP'18: PROCEEDINGS OF THE 20TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2018,
  • [45] Equivalence Checking of Dynamic Quantum Circuits
    Hong, Xin
    Feng, Yuan
    Li, Sanjiang
    Ying, Mingsheng
    2022 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, ICCAD, 2022,
  • [46] Using SAT for combinational equivalence checking
    Goldberg, EI
    Prasad, MR
    Brayton, RK
    DESIGN, AUTOMATION AND TEST IN EUROPE, CONFERENCE AND EXHIBITION 2001, PROCEEDINGS, 2001, : 114 - 121
  • [47] Equivalence Checking For Synchronous Elastic Circuits
    Wijayasekara, Vidura
    Srinivasan, Sudarshan K.
    2013 ELEVENTH ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CODESIGN (MEMOCODE 2013), 2013, : 109 - 118
  • [48] Equivalence checking of two statechart specifications
    Park, MH
    Bang, KS
    Choi, JY
    Kang, I
    11TH IEEE INTERNATIONAL WORKSHOP ON RAPID SYSTEM PROTOTYPING, PROCEEDINGS, 2000, : 46 - 51
  • [49] Equivalence checking using cuts and heaps
    Kuehlmann, A
    Krohm, F
    DESIGN AUTOMATION CONFERENCE - PROCEEDINGS 1997, 1997, : 263 - 268
  • [50] High Coverage Concolic Equivalence Checking
    Roy, Pritam
    Chaki, Sagar
    Chauhan, Pankaj
    2019 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2019, : 462 - 467
12345