Owicki/Gries in Isabelle/HOL

被引：0
|
作者：
Nipkow, T [1 ]
Nieto, LP [1 ]
机构：
[1] Tech Univ Munich, Inst Informat, D-80290 Munich, Germany
来源：
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING | 1999年 / 1577卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a formalization of the Gries/Owicki method for correctness proofs of concurrent imperative programs with shared variables in the theorem prover Isabelle/HOL. Syntax, semantics and proof rules are defined in higher-order logic. The correctness of the proof rules w.r.t. the semantics is proved. The verification of some typical example programs like producer/consumer is presented.
引用
收藏
页码：188 / 203
页数：16
相关论文
共 50 条
  • [1] Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL
    Dalvandi, Sadegh
    Dongol, Brijesh
    Doherty, Simon
    Wehrheim, Heike
    Journal of Automated Reasoning, 2022, 66 (01): : 141 - 171
  • [2] Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL
    Sadegh Dalvandi
    Brijesh Dongol
    Simon Doherty
    Heike Wehrheim
    Journal of Automated Reasoning, 2022, 66 : 141 - 171
  • [3] Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
    Dalvandi, Sadegh
    Dongol, Brijesh
    Doherty, Simon
    Wehrheim, Heike
    JOURNAL OF AUTOMATED REASONING, 2022, 66 (01) : 141 - 171
  • [4] EXTENDING THE THEORY OF OWICKI AND GRIES WITH A LOGIC OF PROGRESS
    Dongol, Brijesh
    Goldson, Doug
    LOGICAL METHODS IN COMPUTER SCIENCE, 2006, 2 (01)
  • [5] Importing HOL into Isabelle/HOL
    Obua, Steven
    Skalberg, Sebastian
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 298 - 302
  • [6] Extending the theory of Owicki and Gries with asynchronous message passing
    Goldson, D
    ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2003, : 532 - 541
  • [7] Owicki-Gries Reasoning for Weak Memory Models
    Lahav, Ori
    Vafeiadis, Viktor
    AUTOMATA, LANGUAGES, AND PROGRAMMING, PT II, 2015, 9135 : 311 - 323
  • [8] Ownership-Based Owicki-Gries Reasoning
    Semenyuk, Mikhail
    Dongol, Brijesh
    38TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, SAC 2023, 2023, : 1685 - 1694
  • [9] An interpretation of Isabelle/HOL in HOL Light
    McLaughlin, Sean
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 192 - 204
  • [10] Safety and Conservativity of Definitions in HOL and Isabelle/HOL
    Kuncar, Ondrej
    Popescu, Andrei
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2 (POPL):
12345