Logic of Programs 1983: Logics of Programs pp 326-340 | Cite as

A verifier for compact parallel coordination programs

  • B. D. Lubachevsky
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 164)


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Clarke, E.M.: Synthesis of resource invariants for concurrent programs. ACM TOPLAS, Vol.2, No.3, July 1980, p. 338–358.Google Scholar
  2. 2.
    Courtois, P.J., Heymans, F., Parnas, D.L.: Concurrent control with "readers" and "writers." Comm. ACM, Vol. 14, No.10 (October 1971), 667–668.Google Scholar
  3. 3.
    Dijkstra, E.M.: Hierarchial orderings of sequential processes. Acta Inf., Vol.1, p. 115–138 (1971).Google Scholar
  4. 4.
    Gottlieb, A., Grishman, R., Kruskal, C.P., McAuliffe, K.P., Rudolph, L., and Snir, M.: The NYU ultracomputer-designing an MIMD shared memory parallel machine. IEEE Trans. on Computer, C-32, No.2 (Feb. 1983).Google Scholar
  5. 5.
    Gottlieb, A., Lubachevsky, B.D., Rudolph, L.: Basic techniques for the efficient coordination of very large numbers of cooperating sequential processors. ACM TOPLAS, Vol.5, No.2, April 1983, p. 164–189.Google Scholar
  6. 6.
    Habermann, A.N.: Synchronization of communicating processes. Comm. ACM, Vol. 15, No. 3 (March 1972), p. 171–176.Google Scholar
  7. 7.
    Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comp. Syst. Sci. 3., 147–195 (1969).Google Scholar
  8. 8.
    Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 125–143 (1977).Google Scholar
  9. 9.
    Lamport, L: Concurrent reading and writing. Comm. ACM., Vol. 20, No. 11, (November 1977), p. 806–811.Google Scholar
  10. 10.
    Lubachevsky, B.D.: An approach to automating the verification of compact parallel coordination programs. Submitted to publication.Google Scholar
  11. 11.
    Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs.I, Acta Inf. 6, p. 319–340, (1976).Google Scholar
  12. 12.
    Owicki, S. Lamport, L.: Proving liveness properties of concurrent programs. ACM TOPLAS, 3, Vol.4 (July 1982).Google Scholar
  13. 13.
    Peterson, G.L.: Concurrent reading while writing. ACM TOPLAS, 1, Vol.5 (January 1983), p. 46–55.Google Scholar
  14. 14.
    Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Comp. Sci., Vol.13 (1981), p. 45–60. 1980, PP. 484–521.Google Scholar
  15. 15.
    Rudolph, L.: Software structures for ultraparallel computings. Ph.D. Thesis, Courant Inst., NYU, 1982.Google Scholar
  16. 16.
    Schwartz, R.L., Melliar-Smith, P.M.: Temporal logic specification of distributed systems. Proc. 2-nd Int. Conf. on Distributed Computing Systems, Paris, April 1981, p. 446–454.Google Scholar
  17. 17.
    Shaw, A.C.: The logical design of operating systems. Prentice-Hall, Englewood, New Jersey, 1974.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • B. D. Lubachevsky
    • 1
  1. 1.Courant Institute of Mathematical SciencesNew York UniversityNew YorkUSA

Personalised recommendations