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 条
  • [31] Semantic Program Alignment for Equivalence Checking
    Churchill, Berkeley
    Padon, Oded
    Sharma, Rahul
    Aiken, Alex
    PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 1027 - 1040
  • [32] Checking equivalence of quantum circuits and states
    Viamontes, George R.
    Markov, Igor L.
    Hayes, John P.
    IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN DIGEST OF TECHNICAL PAPERS, VOLS 1 AND 2, 2007, : 69 - +
  • [33] Equivalence Checking of Sequential Quantum Circuits
    Wang, Qisheng
    Li, Riling
    Ying, Mingsheng
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2022, 41 (09) : 3143 - 3156
  • [34] Distributed On-the-Fly Equivalence Checking
    Joubert, Christophe
    Mateescu, Radu
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 128 (03) : 47 - 62
  • [35] Data-Driven Equivalence Checking
    Sharma, Rahul
    Schkufza, Eric
    Churchill, Berkeley
    Aiken, Alex
    ACM SIGPLAN NOTICES, 2013, 48 (10) : 391 - 406
  • [36] Advanced Equivalence Checking for Quantum Circuits
    Burgholzer, Lukas
    Wille, Robert
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2021, 40 (09) : 1810 - 1824
  • [37] Equivalence checking using independent cuts
    Xu, Z
    Yan, XL
    Lu, YJ
    Ge, HT
    ATS 2003: 12TH ASIAN TEST SYMPOSIUM, PROCEEDINGS, 2003, : 482 - 485
  • [38] Equivalence checking using structural methods
    Kunz, Wolfgang
    Stoffel, Dominik
    IT - Information Technology, 2001, 43 (01): : 8 - 15
  • [39] Equivalence Checking using Trace Partitioning
    Mukherjee, Rajdeep
    Kroening, Daniel
    Melham, Tom
    Srivas, Mandayam
    2015 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI, 2015, : 13 - 18
  • [40] Partial Equivalence Checking of Quantum Circuits
    Chen, Tian-Fu
    Jiang, Jie-Hong R.
    Hsieh, Min-Hsiu
    2022 IEEE INTERNATIONAL CONFERENCE ON QUANTUM COMPUTING AND ENGINEERING (QCE 2022), 2022, : 594 - 604
12345