Abstract
This paper focusses on the mathematical theory of state-based reasoning about program constructs solely through specifications of their parts, without any reliance on their implementation mechanism. That is, the semantic foundations of compositional state-based reasoning about concurrency. The main advantages of a purely semantic approach are that:
-
it highlights the very concept of compositional state-based reasoning about concurrency without any syntactic overhead, and
-
it serves as a basis for the encoding of the program semantics and corresponding proof rules inside tools such as PVS which support program verification.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky. Domain Theory in Logical Form. Proceedings, Annual Symposium on Logic in Computer Science, pp. 47–53, IEEE CS, 1987. Extended version in Annals of Pure and Applied Logic, 51: 1–77, 1991.
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.
R.P. Kurshan and L. Lamport. Verification of a multiplier: 64 bits and beyond. Proceedings of the 5th International Conference on Computer-Aided Verification(CAV94).
W.-P. de Roever, F.S. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel,and J. Zwiers. Concurrency Verification: From Noncompositional to Compositional Proof Methods Submitted for publication in 1998.
J. Zwiers. Compositionality and Partial Correctness LNCS 321. Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Boer, F.S., de Roever, W.P. (1998). Compositional proof methods for concurrency: A semantic approach. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_25
Download citation
DOI: https://doi.org/10.1007/3-540-49213-5_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65493-3
Online ISBN: 978-3-540-49213-9
eBook Packages: Springer Book Archive