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
    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
    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
    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
    Journal of Logic and Computation, 2002, 12 (04) : 549 - 560
  • [5] VERIFICATION OF PROTOCOLS USING SYMBOLIC EXECUTION
    BRAND, D
    JOYNER, WH
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1978, 2 (4-5): : 351 - 360
  • [6] FORMAL PROGRAM VERIFICATION USING SYMBOLIC EXECUTION
    DANNENBERG, RB
    ERNST, GW
    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
    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
    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
    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
    Software & Systems Modeling, 2018, 17 : 815 - 849
12345