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

共 27 条

[1] ANDERSEN F, 1994, LECT NOTES COMP SCI, V780, P1
[2] APT KR, 1991, VERIFICATION SEQUENT
[3] MECHANIZING CSP TRACE THEORY IN HIGHER-ORDER LOGIC
CAMILLERI, AJ
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (09) : 993 - 1004
[4] CHETALI B, 1997, LECT NOTES COMP SCI, V1275, P69
[5] de Boer F. S, 1997, LNCS, V1313, P515
[6] DUTERTRE B, 1997, LECT NOTES COMPUTER, V1275, P121
[7] ENGBERG U, 1992, LNCS, V663, P44
[8] MECHANICALLY VERIFYING CONCURRENT PROGRAMS WITH THE BOYER-MOORE PROVER
GOLDSCHLAG, DM
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (09) : 1005 - 1023
[9] Gordon M. J., 1993, INTRO HOL THEOREM PR
[10] GORDON MJC, 1989, CURRENT TRENDS HARDW

← 1 2 3 →