Abstract
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.
This work has been realized as part of the author’s PhD at the Computer Science Faculty of the Technical University of Munich.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
W.-P. de Roever, F. S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods, volume 54 of Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
S. O. Ehmety and L. C. Paulson. Program composition in Isabelle/UNITY. In M. Charpentier and B. Sanders, editors, Formal Methods for Parallel Programming: Theory and Application, 2002.
C. Flanagan, S. Freund, and S. Qadeer. Thread-modular verification for sharedmemory programs. In European Symposium on Programming, volume 2305 of LNCS, pages 262–277. Springer-Verlag, 2002.
J. Hooman. Developing proof rules for distributed real-time systems with PVS. In Proc. Workshop on Tool Support for System Development and Verification, volume 1 of BISS Monographs, pages 120–139. Shaker Verlag, 1998.
C. B. Jones. Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–619, 1983.
K. L. McMillan. Circular compositional reasoning about liveness. In Advances in Hardware Design and Verification Methods: IFIP WG10.5 (CHARME’99), volume 1703 of LNCS, pages 342–345. Springer-Verlag, 1999.
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL-A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002.
T. Nipkow and L. Prensa Nieto. Owicki/Gries in Isabelle/HOL. In J.-P. Finance, editor, Fundamental Approaches to Software Engineering, volume 1577 of LNCS, pages 188–203. Springer-Verlag, 1999.
L. C. Paulson. Mechanizing a theory of program composition for UNITY. ACM Transactions on Programming Languages and Systems, 23(6):1–30, 2001.
L. Prensa Nieto. Completeness of the Owicki-Gries system for parameterized parallel programs. In M. Charpentier and B. Sanders, editors, 6th International Workshop on Formal Methods for Parallel Programming: Theory and Applications. Held in conjunction with the 15th International Parallel and Distributed Processing Symposium. IEEE CS Press, 2001.
L. Prensa Nieto. Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL. PhD thesis, Technische Universität München, 2002. Available at http://tumb1.biblio.tu-muenchen.de/publ/diss/allgemein.html.
J. Rushby. Formal verification of McMillan’s compositional assume-guarantee rule. Technical report, Sept. 2001.
C. Stirling. A generalization of Owicki-Gries’s Hoare logic for a concurrent while language. Theoretical Computer Science, 58:347–359, 1988.
Q. Xu, W.-P. de Roever, and J. He. Rely-guarantee method for verifying shared variable concurrent programs. Technical Report 9502, Christian-Albrechts-Universität Kiel, March 1995.
Q. Xu, W.-P. de Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149–174, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nieto, L.P. (2003). The Rely-Guarantee Method in Isabelle/HOL. In: Degano, P. (eds) Programming Languages and Systems. ESOP 2003. Lecture Notes in Computer Science, vol 2618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36575-3_24
Download citation
DOI: https://doi.org/10.1007/3-540-36575-3_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00886-6
Online ISBN: 978-3-540-36575-4
eBook Packages: Springer Book Archive