Abstract
This paper introduces a semantic analysis of the Rely-Guarantee (R-G) approach to the compositional verification of shared-variable concurrency. The main contribution is a new completeness proof.
Chapter PDF
Similar content being viewed by others
References
M. Abadi and G. D. Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3–30, 1993.
G. Berry. The Constructive Semantics of Esterel. Book in preparation, http://www-sop.inria.fr/meije/esterel/doc/main-papers.html, 1999.
S. Brookes. A fully abstract semantics of a shared variable parallel language. In Proceedings 8th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pages 98–109, 1993.
F.S. de Boer, J.N. Kok, C. Palamedessi, and J.J.M.M. Rutten. The failure of failures: towards a paradigm for asynchronous communication. In Baeten and Groote, editors, CONCUR’91, LNCS 527. Springer-Verlag, 1991.
W.-P. de Roever. The quest for compositionality-a survey of assertion-based proof systems for concurrent programs, part 1: Concurrency based on shared variables. In Proc. of IFIP Working Conf, The Role of Abstract Models in Computer Science, North-Holland, 1985.
W.-P. de Roever, F.S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: An Introduction to State-based Methods. To appear.
R.W. Floyd. Assigning meanings to programs. In Proceedings AMS Symp. Applied Mathematics, volume 19, pages 19–31, Providence, R.I., 1967. American Mathematical Society.
J. Hooman. Compositional Verification of Real-Time Applications. In W.-P. de Roever, H. Langmaack, and A. Pnueli (eds.) Compositionality: The Significant Difference. International Symposium, COMPOS’97, Bad Malente, Germany, September 8-12, 1997. pp. 130–149, Springer-Verlag, LNCS 1536, 1998.
C.B. Jones. Development methods for computer programs including a notion of interference. PhD thesis, Oxford University Computing Laboratory, 1981.
C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–619, 1983.
L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3), pp. 872–923, 1994.
J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engeneering, 7(7):417–426, 1981.
E. Stark. A proof technique for rely/guarantee properties. In Proceedings of 5th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 206, pages 369–391. Springer-Verlag, 1985.
Q. Xu. A theory of state-based parallel programming. DPhil. Thesis, Oxford University computing Laboratory, 1992.
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
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Boer, F.S., Hannemann, U., de Roever, W.P. (1999). Formal justification of the rely-guarantee paradigm for shared-variable concurrency: a semantic approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_16
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive