Flat acceleration in symbolic model checking

被引：0
|
作者：
Bardin, S
Finkel, A
Leroux, J
Schnoebelen, P
机构：
[1] ENS, LSV, F-94235 Cachan, France
[2] CNRS, UMR 8643, F-94235 Cachan, France
[3] INRISA, INRIA, Vertecs Project, F-35042 Rennes, France
来源：
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS | 2005年 / 3707卷
关键词：
verification of infinite-state systems; symbolic model checking; acceleration;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Symbolic model checking provides partially effective verification procedures that can handle systems with an infinite state space. So-called "acceleration techniques" enhance the convergence of fixpoint computations by computing the transitive closure of some transitions. In this paper we develop a new framework for symbolic model checking with accelerations. We also propose and analyze new symbolic algorithms using accelerations to compute reachability sets.
引用
收藏
页码：474 / 488
页数：15
相关论文
共 50 条
  • [1] Symbolic model checking
    McMillan, KL
    [J]. VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
  • [2] Interpolants and symbolic model checking
    McMillan, K. L.
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2007, 4349 : 89 - 90
  • [3] On partitioning and symbolic model checking
    Iyer, S
    Sahoo, D
    Emerson, EA
    Jain, J
    [J]. FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 497 - 511
  • [4] On partitioning and symbolic model checking
    Iyer, S
    Sahoo, D
    Emerson, EA
    Jain, J
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2005, 25 (05) : 780 - 788
  • [5] Symbolic model checking APSL
    Liu, Wanwei
    Wang, Ji
    Chen, Huowang
    Ma, Xiaodong
    Wang, Zhaofei
    [J]. FRONTIERS OF COMPUTER SCIENCE IN CHINA, 2009, 3 (01): : 130 - 141
  • [6] Symbolic model checking APSL
    Liu, Wanwei
    Wang, Ji
    Chen, Huowang
    Ma, Xiaodong
    [J]. TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 39 - 46
  • [7] Symbolic model checking APSL
    Wanwei Liu
    Ji Wang
    Huowang Chen
    Xiaodong Ma
    Zhaofei Wang
    [J]. Frontiers of Computer Science in China, 2009, 3 : 130 - 141
  • [8] Lazy symbolic model checking
    Yang, J
    Tiemeyer, A
    [J]. 37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 35 - 38
  • [9] Symbolic Causality Checking Using Bounded Model Checking
    Beer, Adrian
    Heidinger, Stephan
    Kuehne, Uwe
    Leitner-Fischer, Florian
    Leue, Stefan
    [J]. MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 203 - 221
  • [10] Unit checking: Symbolic model checking for a unit of code
    Gunter, E
    Peled, D
    [J]. VERIFICATION: THEORY AND PRACTICE: ESSAYS DEDICATED TO ZHOAR MANNA ON THE OCCASION OF HIS 64TH BIRTHDAY, 2003, 2772 : 548 - 567
12345