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 条
  • [21] Verifying Parallel Code After Refactoring Using Equivalence Checking
    Moria Abadi
    Sharon Keidar-Barner
    Dmitry Pidan
    Tatyana Veksler
    International Journal of Parallel Programming, 2019, 47 : 59 - 73
  • [22] Formula-dependent equivalence for compositional CTL model checking
    Aziz, A
    Shiple, T
    Singhal, V
    Brayton, R
    Sangiovanni-Vincentelli, A
    FORMAL METHODS IN SYSTEM DESIGN, 2002, 21 (02) : 193 - 224
  • [23] Enhancing active model learning with equivalence checking using simulation relations
    Natasha Yogananda Jeppu
    Tom Melham
    Daniel Kroening
    Formal Methods in System Design, 2022, 61 : 164 - 197
  • [24] Generalized Affine Equivalence Checking of Boolean Functions via Reachability Analysis
    Zeng, Xiao
    Liang, Huijun
    Yuan, Jun
    Song, Xiaoyu
    Yang, Guowu
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2023, 42 (09) : 2966 - 2979
  • [25] Enhancing active model learning with equivalence checking using simulation relations
    Yogananda Jeppu, Natasha
    Melham, Tom
    Kroening, Daniel
    FORMAL METHODS IN SYSTEM DESIGN, 2022, 61 (2-3) : 164 - 197
  • [26] Translation Validation of Transformations of Embedded System Specifications using Equivalence Checking
    Banerjee, Kunal
    Mandal, Chittaranjan
    Sarkar, Dipankar
    2015 IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI, 2015, : 183 - 186
  • [27] Formal Verification of Heuristic Autonomous Intersection Management Using Statistical Model Checking
    Chouhan, Aaditya Prakash
    Banda, Gourinath
    SENSORS, 2020, 20 (16) : 1 - 25
  • [28] Equivalence between model-checking flat counter systems and presburger arithmeti
    Demri, Stéphane
    Dhar, Amit Kumar
    Sangnier, Arnaud
    1600, Springer Verlag (8762): : 85 - 97
  • [29] Equivalence between model-checking flat counter systems and Presburger arithmetic
    Demri, Stephane
    Dhar, Amit Kumar
    Sangnier, Arnaud
    THEORETICAL COMPUTER SCIENCE, 2018, 735 : 2 - 23
  • [30] A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata
    Koenig, Barbara
    Kuepper, Sebastian
    SOFT COMPUTING, 2018, 22 (04) : 1103 - 1120
12345