TY - GEN
T1 - Owicki/Gries in Isabelle/HOL
AU - Nipkow, Tobias
AU - Nieto, Leonor Prensa
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84947908053&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-49020-3_13
DO - 10.1007/978-3-540-49020-3_13
M3 - Conference contribution
AN - SCOPUS:84947908053
SN - 3540657185
SN - 9783540657187
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 188
EP - 203
BT - Fundamental Approaches to Software Engineering - 2nd Intrnational Conference, FASE 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999, Proceedings
A2 - Finance, Jean-Pierre
PB - Springer Verlag
T2 - 2nd International Conference on Fundamental Approaches to Software Engineering, FASE 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999
Y2 - 22 March 1999 through 28 March 1999
ER -