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 条
  • [21] 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
  • [22] Verification of Java']Java programs using symbolic execution and invariant generation
    Pasareanu, CS
    Visser, W
    [J]. MODEL CHECKING SOFTWARE, 2004, 2989 : 164 - 181
  • [23] Formal Verification of AUTOSAR Watchdog Manager Module Using Symbolic Execution
    Ahmed, Mazen
    Safar, Mona
    [J]. 2018 30TH INTERNATIONAL CONFERENCE ON MICROELECTRONICS (ICM), 2018, : 240 - 243
  • [24] Supporting symbolic verification in concurrent engineering
    Loumi, C
    [J]. ADVANCES IN CONCURRENT ENGINEERING: CE97, 1997, 97 : 263 - 269
  • [25] No Panic! Verification of Rust Programs by Symbolic Execution
    Lindner, Marcus
    Aparicius, Jorge
    Lindgren, Per
    [J]. 2018 IEEE 16TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2018, : 108 - 114
  • [26] SYMBOLIC EXECUTION SYSTEMS - A REVIEW
    COWARD, PD
    [J]. SOFTWARE ENGINEERING JOURNAL, 1988, 3 (06): : 229 - 239
  • [27] Rule-based Verification of Network Protocol Implementations using Symbolic Execution
    Song, JaeSeung
    Ma, Tiejun
    Cadar, Cristian
    Pietzuch, Peter
    [J]. 2011 20TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS (ICCCN), 2011,
  • [28] 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,
  • [29] PBMC: Symbolic Slicing for the Verification of Concurrent Programs
    Saissi, Habib
    Bokor, Peter
    Suri, Neeraj
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 344 - 360
  • [30] SEIF: Augmented Symbolic Execution for Information Flow Verification
    Ryan, Kaki
    Gregoire, Matthew
    Sturton, Cynthia
    [J]. PROCEEDINGS OF THE 12TH INTERNATIONAL WORKSHOP ON HARDWARE AND ARCHITECTURAL SUPPORT FOR SECURITY AND PRIVACY, HASP 2023, 2023, : 1 - 9
12345