×

An approach to automating the verification of compact parallel coordination programs. I. (English) Zbl 0522.68017


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N25 Theory of operating systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ashcroft, E.A.: Proving assertions about parallel programs. Journ. Comput. System Sci. 10, 110-135 (1975) · Zbl 0299.68013
[2] Ben-Ari, M.: Temporal logic proofs of concurrent programs. Dept. Appl. Math., Weizmann Institute of Science, Report CS82-12, 1982 · Zbl 0534.68005
[3] Clarke, E.M.: Synthesis of resource invariants for concurrent programs. ACM Trans. on Programming Languages and Systems. 2 (3), 338-358 (1980) · Zbl 0468.68024
[4] Courtois, P.J., Heymans, F., Parnas, D.L.: Concurrent control with ?readers? and ?writers?. Comm. ACM 14, 667-668 (1971)
[5] Dijkstra, E.M.: Hierarchical orderings of sequential processes. Acta Informat. 1, 115-138 (1971)
[6] Genrich, H.J., Lautenbach, K.: System modeling with high-level Petri Nets. Theor. Comput. Sci. 13, 109-136 (1981) · Zbl 0454.68052
[7] Gottlieb, A., Grishman, R., Kruskal, C.P., McAuliffe, K.P., Rudolph, L., Snir, M.: The NYU Ultracomputer-designing an MIMD shared memory parallel computer. IEEE Trans. Computers, Vol. C-32, No. 2, February 1983
[8] Gottlieb, A., Lubachevsky, B.D., Rudolph, L.: Basic techniques for the efficient coordination of very large numbers of cooperating sequential processors. ACM Trans, on Comput. Lang. Sys. 5 (2), 164-189 (1983) · Zbl 0511.68012
[9] Habermann, A.N.: Synchronization of communicating processes. Comm. ACM. 15 (3), 171-176 (1972)
[10] Hopcroft, J., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135-159 (1979) · Zbl 0466.68048
[11] Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. System. Sci. 3, 147-195 (1969) · Zbl 0198.32603
[12] Kwong, Y.S.: On the absence of livelocks in parallel programs. In: Semantics of Concurrent Computation. (G. Goos, J. Hartmanis, eds.) Proc. of the Int. Symp., Lecture Notes in Computer Science 70, pp. 172-190. Berlin-Heidelberg-New York: Springer 1979
[13] Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 125-143 (1977) · Zbl 05341279
[14] Lubachevsky, B.D.: Verification of several parallel coordination programs based on descriptions of their reachability sets. Ultracomputer Note # 33, Courant Institute, New York University, July, 1981
[15] Morris, J.M.: A starvation-free solution to the mutual exclusion problem. Information Processing Lett. 8, 76-80 (1979) · Zbl 0397.68036
[16] Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, No. 5, p. 279-285 (May 1976) · Zbl 0322.68010
[17] Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. I. Acta Informat. 6, 319-340 (1976) · Zbl 0324.68007
[18] Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang, and Syst. 3, vol. 4 (July 1982) · Zbl 0483.68013
[19] Park, D.: Fixpoint induction and proofs of program properties. In: Machine Intelligence (B. Meltzer and D. Michie, eds.) 5, 59-78. Edinburgh: University Press 1969 · Zbl 0219.68007
[20] Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput Sci. 13, 45-60 (1981) · Zbl 0441.68010
[21] Rudolph, L.: Software structures for ultraparallel computings. Ph.D. Thesis, Courant Inst., NYU, 1982
[22] Schwartz, J.T.: Ultracomputers. ACM Trans, on Prog. Lang. Sys. pp. 484-521 (1980)
[23] Schwartz, R.L., and Melliar-Smith, P.M.: Temporal logic specification of distributed systems. Proc. 2-nd Int. Conf. on Distributed Computing Systems, pp. 446-454. Paris, April 1981
[24] Shaw, A.C.: The logical design of operating systems Englwood Cliffs: Prentice-Hall, 1974
[25] Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285-309 · Zbl 0064.26004
[26] Thau, R.: Private communication.
[27] van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct concurrent programs. Acta Informat. 12, 1-31 (1979) · Zbl 0395.68029
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.