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] SE3: Sequential Equivalence Checking for Non-Cycle-Accurate Design Transformations
    Li, You
    Zhao, Guannan
    He, Yunqi
    Zhou, Hai
    2023 60TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, DAC, 2023,
  • [32] Bounded Rational Search for On-the-Fly Model Checking of LTL Properties
    Behjati, Razieh
    Sirjani, Marjan
    Ahmadabadi, Majid Nili
    FUNDAMENTALS OF SOFTWARE ENGINEERING, 2010, 5961 : 292 - 307
  • [33] A nested depth first search algorithm for model checking with symmetry reduction
    Bosnacki, D
    FORMAL TECHNIQUE FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2002, PROCEEDINGS, 2002, 2529 : 65 - 80
  • [34] Formal Verification of Code Motion Techniques Using Data-Flow-Driven Equivalence Checking
    Karfa, Chandan
    Mandal, Chittaranjan
    Sarkar, Dipankar
    ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2012, 17 (03)
  • [35] Symbolic Reachability Analysis of Distributed Systems using Narrowing and Heuristic Search
    Kang, Byeongjee
    Bae, Kyungmin
    PROCEEDINGS OF THE 8TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2022, 2022, : 34 - 44
  • [36] Solving Complex Path Conditions through Heuristic Search on Induced Polytopes
    Dinges, Peter
    Agha, Gul
    22ND ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (FSE 2014), 2014, : 425 - 436
  • [37] Precise Data Race detection in a Relaxed Memory Model using Heuristic-based Model Checking
    Kim, KyungHee
    Yavuz-Kahveci, Tuba
    Sanders, Beverly A.
    2009 IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 495 - 499
  • [38] Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties
    Li, Lvzhou
    Feng, Yuan
    INFORMATION AND COMPUTATION, 2015, 244 : 229 - 244
  • [39] A case study of planning for smart factories: Model checking and Monte Carlo search for the rescue
    Edelkamp S.
    Greulich C.
    International Journal on Software Tools for Technology Transfer, 2018, 20 (5) : 515 - 528
  • [40] Similarity-Based Search for Model Checking: A Pilot Study with Java']Java PathFinder
    Ibrahimov, Elmin
    Wang, Jixing
    Zhou, Zhi Quan
    2013 13TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC), 2013, : 238 - 244
12345