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.
CITATION STYLE
Nipkow, T., & Nieto, L. P. (1999). Owicki/Gries in Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1577, pp. 188–203). Springer Verlag. https://doi.org/10.1007/978-3-540-49020-3_13
Mendeley helps you to discover research relevant for your work.