The rely-guarantee method in Isabelle/HOL

Abstract

We present the formalization of the rely-guarantee method in the theorem prover Isabelle/HOL. This method consists of a Hoare-like system of rules to verify concurrent imperative programs with shared variables in a compositional way. Syntax, semantics and proof rules are defined in higher-order logic. Soundness of the proof rules w.r.t. the semantics is proven mechanically. Also parameterized programs, where the number of parallel components is a parameter, are included in the programming language and thus can be verified directly in the system. We prove that the system is complete for parameterized programs. Finally, we show by an example how the formalization can be used for verifying concrete programs. © Springer-Verlag Berlin Heidelberg 2003.