Abstract
We propose a specification language for shared-variable concurrent programs based on Morgan's specification statement [Mor89]. A denotational semantics is given in terms of transition traces (sequences of pairs of states) following [Bro93]. A context-sensitive notion of approximation between specifications is presented which permits modular verification through stepwise program transformation. We argue that the resulting framework also supports program development through stepwise refinement.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15:73–132, 1993.
R.J.R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593–624, 1988.
H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Sixteenth Annual ACM Symposium on Theory of Computing, pages 51–63. ACM, April 1984.
S. D. Brookes. Full abstraction for a shared-variable parallel language. In Proceedings 8th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1993.
E. W. Dijkstra. A discipline of programming. Prentice Hall, 1976.
J. Dingel. Towards a theory for shared-variable concurrent programming. Thesis proposal, Carnegie Mellon University, 1996.
O. Grumberg and D. Long. Model checking and modular verification. In CONCUR '91, LNCS 527. Springer Verlag, 1991.
C. B. Jones. Specification and design of (parallel) programs. In IFIF '83, 1983.
K. G. Larsen. A context dependent equivalence between processes. Theoretical Computer Science, 49(2):185–216, 1987.
Robin Milner. Communication and Concurrency. Prentise Hall International, 1989.
J.M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287–306, December 1987.
C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3), January 1989.
C. Morgan. Programming from specifications. Prentice Hall, 1994.
S.S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319–340, 1976.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In K.R. Apt, editor, Logics and Models of Concurrent Systems, NATO ASI F13, pages 123–144. Springer Verlag, 1985.
C. Stirling. A generalization of Owicki-Gries' Hoare logic for a concurrent while language. Theoretical Computer Science, 89:347–359, 1988.
K. StØlen. A method for the development of totally correct shared-state parallel programs. In CONCUR '91. Springer Verlag, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dingel, J. (1996). Modular verification for shared-variable concurrent programs. In: Montanari, U., Sassone, V. (eds) CONCUR '96: Concurrency Theory. CONCUR 1996. Lecture Notes in Computer Science, vol 1119. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61604-7_85
Download citation
DOI: https://doi.org/10.1007/3-540-61604-7_85
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61604-7
Online ISBN: 978-3-540-70625-0
eBook Packages: Springer Book Archive