Verifying concurrent systems with symbolic execution

被引：9
|
作者：
Balser, Michael [1 ]
Duelli, Christoph [1 ]
Reif, Wolfgang [1 ]
Schellhorn, Gerhard [1 ]
机构：
[1] LSP, Universität Augsburg, D-86135 Augsburg, Germany
来源：
Journal of Logic and Computation | 2002年 / 12卷 / 04期
关键词：
Interactive theorem prover - Parallel programs - Program counter variables - Sequential programs symbolic execution - Temporal logic;
D O I：
10.1093/logcom/12.4.549
中图分类号：
学科分类号：
摘要：
引用
收藏
页码：549 / 560
相关论文
共 50 条
  • [1] Interactive verification of concurrent systems using symbolic execution
    Baeumler, Simon
    Balser, Michael
    Nafz, Florian
    Reif, Wolfgang
    Schellhorn, Gerhard
    [J]. AI COMMUNICATIONS, 2010, 23 (2-3) : 285 - 307
  • [2] SYMBOLIC EXECUTION OF CONCURRENT SYSTEMS USING PETRI NETS
    GHEZZI, C
    MANDRIOLI, D
    MORASCA, S
    PEZZE, M
    [J]. COMPUTER LANGUAGES, 1989, 14 (04): : 263 - 281
  • [3] Verifying Systems Rules Using Rule-Directed Symbolic Execution
    Cui, Heming
    Hu, Gang
    Wu, Jingyue
    Yang, Junfeng
    [J]. ACM SIGPLAN NOTICES, 2013, 48 (04) : 329 - 341
  • [4] Dynamic Symbolic Execution of Distributed Concurrent Objects
    Griesmayer, Andreas
    Aichernig, Bernhard
    Johnsen, Einar Broch
    Schlatte, Rudolf
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 225 - 230
  • [5] Parallel SMT Solving and Concurrent Symbolic Execution
    Rakadjiev, Emil
    Shimosawa, Taku
    Mine, Hiroshi
    Oshima, Satoshi
    [J]. 2015 IEEE TRUSTCOM/BIGDATASE/ISPA, VOL 3, 2015, : 17 - 26
  • [6] Verifying Information Flow Properties of Firmware using Symbolic Execution
    Subramanyan, Pramod
    Malik, Sharad
    Khattri, Hareesh
    Maiti, Abhranil
    Fung, Jason
    [J]. PROCEEDINGS OF THE 2016 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2016, : 337 - 342
  • [7] SYMBOLIC EXECUTION SYSTEMS - A REVIEW
    COWARD, PD
    [J]. SOFTWARE ENGINEERING JOURNAL, 1988, 3 (06): : 229 - 239
  • [8] SYMAC: Symbolic Execution Augmented with Concurrent Coverage Criteria
    Zhou, Yong
    Zhang, Li
    Li, Haoyu
    [J]. PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING (CSSE 2019), 2019,
  • [9] VALIDATION OF CONCURRENT ADA PROGRAMS USING SYMBOLIC EXECUTION
    MORASCA, S
    PEZZE, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 387 : 467 - 486
  • [10] Generic tools for verifying concurrent systems
    Cleaveland, R
    Sims, ST
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2002, 42 (01) : 39 - 47
12345