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 条
  • [31] A GENERALIZATION OF OWICKI-GRIES HOARE LOGIC FOR A CONCURRENT WHILE LANGUAGE
    STIRLING, C
    THEORETICAL COMPUTER SCIENCE, 1988, 58 (1-3) : 347 - 359
  • [32] Comprehending Isabelle/HOL's Consistency
    Kuncar, Ondrej
    Popescu, Andrei
    PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2017): 26TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2017, 10201 : 724 - 749
  • [33] A Modular Formalization of Superposition in Isabelle/HOL
    Desharnais, Martin
    Toth, Balazs
    Waldmann, Uwe
    Blanchette, Jasmin
    Tourret, Sophie
    Leibniz International Proceedings in Informatics, LIPIcs, 309
  • [34] Fast Machine Words in Isabelle/HOL
    Lochbihler, Andreas
    INTERACTIVE THEOREM PROVING, ITP 2018, 2018, 10895 : 388 - 410
  • [35] A Denotational Semantics of Solidity in Isabelle/HOL
    Marmsoler, Diego
    Brucker, Achim D.
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2021), 2021, 13085 : 403 - 422
  • [36] Automating Free Logic in Isabelle/HOL
    Benzmueller, Christoph
    Scott, Dana
    MATHEMATICAL SOFTWARE, ICMS 2016, 2016, 9725 : 43 - 50
  • [37] Extracting a normalization algorithm in Isabelle/HOL
    Berghofer, S
    TYPES FOR PROOFS AND PROGRAMS, 2006, 3839 : 50 - 65
  • [38] Verified Real Asymptotics in Isabelle/HOL
    Eberl, Manuel
    PROCEEDINGS OF THE 2019 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC '19), 2019, : 147 - 154
  • [39] On the mechanization of real analysis in Isabelle/HOL
    Fleuriot, JD
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 145 - 161
  • [40] Formalizing O notation in Isabelle/HOL
    Avigad, J
    Donnelly, K
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 357 - 371
12345