A static analysis of CSP programs
A static analysis is proposed as a method of reducing complexity of the correctness proofs of CSP programs. This analysis is based on considering all possible sequences of communications which can arise in computations during which the boolean guards are not interpreted. Several examples are provided which clarify its various aspects.
Unable to display preview. Download preview PDF.
- [AFR]K.R. APT, N. FRANCEZ & W.P. DE ROEVER, A proof system for communicating sequential processes, TOPLAS, vol. 2, No 3, pp. 359–385, 1980.Google Scholar
- [D]E.W. DIJKSTRA, A correctness proof for communicating processes: a small exercise, in: E.W. Dijkstra, Selected writings on computing: a personal perspective, Springer Verlag, New York, pp. 259–263, 1982.Google Scholar
- [EF]T. ELRAD & N. FRANCEZ, Decomposition of distributed programs into communication-closed layers, to appear in SCP.Google Scholar
- [H]C.A.R. HOARE, Communicating sequential processes, CACM, vol. 21, No 8, pp. 666–677, 1978.Google Scholar
- [H1]C.A.R. HOARE, A model for communicating sequential processes, in: R.M. McKeag, A.M. McNaughton, Eds., On the construction of programs, Cambridge University Press, pp. 229–243, 1980.Google Scholar
- [LG]G. LEVIN & D. GRIES, A proof technique for communicating sequential processes, Acta Informatica, vol. 15, No 3, pp. 281–302, 1981.Google Scholar
- [OL]S. OWICKI & L. LAMPORT, Proving liveness properties of concurrent programs, TOPLAS, vol. 4, No 3, pp. 455–495, 1982.Google Scholar
- [T]R.N. TAYLOR, A general purpose algorithm for analyzing concurrent programs, CACM, vol. 26, No 5, pp. 362–376, 1983.Google Scholar