Interactive verification of concurrent systems using symbolic execution

被引：9
|
作者：
Baeumler, Simon [1 ]
Balser, Michael [1 ]
Nafz, Florian [1 ]
Reif, Wolfgang [1 ]
Schellhorn, Gerhard [1 ]
机构：
[1] Univ Augsburg, Lehrstuhl Softwaretech & Programmiersprachen, D-86135 Augsburg, Germany
来源：
AI COMMUNICATIONS | 2010年 / 23卷 / 2-3期
关键词：
Temporal logic; interactive verification; compositional reasoning; theorem prover; LOGIC;
D O I：
10.3233/AIC-2010-0458
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This paper presents an interactive proof method for the verification of temporal properties of concurrent systems based on symbolic execution. Symbolic execution is a well known and very intuitive strategy for the verification of sequential programs. We have carried over this approach to the interactive verification of arbitrary linear temporal logic properties of ( infinite state) parallel programs. The resulting proof method is very intuitive to apply and can be automated to a large extent. It smoothly combines first-order reasoning with reasoning in temporal logic. The proof method has been implemented in the interactive verification environment KIV and has been used in several case studies.
引用
收藏
页码：285 / 307
页数：23
相关论文
共 50 条
  • [1] SYMBOLIC EXECUTION OF CONCURRENT SYSTEMS USING PETRI NETS
    GHEZZI, C
    MANDRIOLI, D
    MORASCA, S
    PEZZE, M
    [J]. COMPUTER LANGUAGES, 1989, 14 (04): : 263 - 281
  • [2] The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more
    Martin Hentschel
    Richard Bubel
    Reiner Hähnle
    [J]. International Journal on Software Tools for Technology Transfer, 2019, 21 : 485 - 513
  • [3] The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more
    Hentschel, Martin
    Bubel, Richard
    Haehnle, Reiner
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2019, 21 (05) : 485 - 513
  • [4] Verifying concurrent systems with symbolic execution
    Balser, Michael
    Duelli, Christoph
    Reif, Wolfgang
    Schellhorn, Gerhard
    [J]. Journal of Logic and Computation, 2002, 12 (04) : 549 - 560
  • [5] VERIFICATION OF PROTOCOLS USING SYMBOLIC EXECUTION
    BRAND, D
    JOYNER, WH
    [J]. COMPUTER NETWORKS AND ISDN SYSTEMS, 1978, 2 (4-5): : 351 - 360
  • [6] FORMAL PROGRAM VERIFICATION USING SYMBOLIC EXECUTION
    DANNENBERG, RB
    ERNST, GW
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1982, 8 (01) : 43 - 52
  • [7] Towards parallel verification of concurrent systems using the Symbolic Observation Graph
    Ouni, Hiba
    Klai, Kais
    Abid, Chiheb Ameur
    Zouari, Belhassen
    [J]. 2019 19TH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD 2019), 2019, : 23 - 32
  • [8] VALIDATION OF CONCURRENT ADA PROGRAMS USING SYMBOLIC EXECUTION
    MORASCA, S
    PEZZE, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 387 : 467 - 486
  • [9] Using dynamic symbolic execution to improve deductive verification
    Vanoverberghe, Dries
    Bjorner, Nikolaj
    de Halleux, Jonathan
    Schulte, Wolfram
    Tillmann, Nikolai
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2008, 5156 : 9 - 25
  • [10] Full contract verification for ATL using symbolic execution
    Bentley James Oakes
    Javier Troya
    Levi Lúcio
    Manuel Wimmer
    [J]. Software & Systems Modeling, 2018, 17 : 815 - 849
12345