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 条
  • [41] VERIFICATION OF SYNCHRONOUS SEQUENTIAL-MACHINES BASED ON SYMBOLIC EXECUTION
    COUDERT, O
    BERTHET, C
    MADRE, JC
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 407 : 365 - 373
  • [42] Compositional verification of asynchronous concurrent systems using CADP
    Garavel, Hubert
    Lang, Frederic
    Mateescu, Radu
    [J]. ACTA INFORMATICA, 2015, 52 (4-5) : 337 - 392
  • [43] Verification of concurrent systems with parametric delays using octahedra
    Clarisó, R
    Cortadella, J
    [J]. ACSD2005: FIFTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2005, : 122 - 131
  • [44] Verification of concurrent systems with parametric delays using octahedra
    Clariso, Robert
    Cortadella, Jordi
    [J]. FUNDAMENTA INFORMATICAE, 2007, 78 (01) : 1 - 33
  • [45] Compositional verification of asynchronous concurrent systems using CADP
    Hubert Garavel
    Frédéric Lang
    Radu Mateescu
    [J]. Acta Informatica, 2015, 52 : 337 - 392
  • [46] ON EQUIVALENT EXECUTION SEMANTICS OF CONCURRENT SYSTEMS
    JANICKI, R
    KOUTNY, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1987, 266 : 89 - 103
  • [47] Symbolic verification of infinite systems using a finite union of DFAs
    Roy, S
    [J]. PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 56 - 66
  • [48] Finding ∀∃ Hyperbugs using Symbolic Execution
    Correnson, Arthur
    Niessen, Tobias
    Finkbeiner, Bernd
    Weissenbacher, Georg
    [J]. Proceedings of the ACM on Programming Languages, 2024, 8 (OOPSLA2)
  • [49] Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution
    Rungta, Neha
    Mercer, Eric G.
    Visser, Willem
    [J]. MODEL CHECKING SOFTWARE, 2009, 5578 : 174 - +
  • [50] Accelerating SoC Security Verification and Vulnerability Detection Through Symbolic Execution
    Tang, Shibo
    Wang, Xingxin
    Gao, Yifei
    Hu, Wei
    [J]. 2022 19TH INTERNATIONAL SOC DESIGN CONFERENCE (ISOCC), 2022, : 207 - 208
12345