Skip to main content
SpringerLink
Log in

A static analysis of CSP programs

  • Conference paper
  • First Online:
Logics of Programs (Logic of Programs 1983)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 164))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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 

  2. 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 

  3. T. ELRAD & N. FRANCEZ, Decomposition of distributed programs into communication-closed layers, to appear in SCP.

    Google Scholar 

  4. C.A.R. HOARE, Communicating sequential processes, CACM, vol. 21, No 8, pp. 666–677, 1978.

    Google Scholar 

  5. 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 

  6. G. LEVIN & D. GRIES, A proof technique for communicating sequential processes, Acta Informatica, vol. 15, No 3, pp. 281–302, 1981.

    Google Scholar 

  7. S. OWICKI & L. LAMPORT, Proving liveness properties of concurrent programs, TOPLAS, vol. 4, No 3, pp. 455–495, 1982.

    Google Scholar 

  8. R.N. TAYLOR, A general purpose algorithm for analyzing concurrent programs, CACM, vol. 26, No 5, pp. 362–376, 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LITP, Université Paris 7, 2, Place Jussieu, 75251, Paris, France

    Krzysztof R. Apt

Authors
  1. Krzysztof R. Apt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Edmund Clarke Dexter Kozen

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Apt, K.R. (1984). A static analysis of CSP programs. In: Clarke, E., Kozen, D. (eds) Logics of Programs. Logic of Programs 1983. Lecture Notes in Computer Science, vol 164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12896-4_351

Download citation

  • DOI: https://doi.org/10.1007/3-540-12896-4_351

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-12896-0

  • Online ISBN: 978-3-540-38775-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation