We present the formalization of the rely-guarantee method in the theorem prover Isabelle/HOL. This method consists of a Hoarelike system of rules to verify concurrent imperative programs with shared variables in a compositional way. Syntax, semantics and proof rules are de.ned 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.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
- The Rely-Guarantee Method in Isabelle/HOL
Leonor Prensa Nieto
- Springer Berlin Heidelberg
Neuer Inhalt/© ITandMEDIA