{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T13:12:02Z","timestamp":1769951522914,"version":"3.49.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1984,8,1]],"date-time":"1984-08-01T00:00:00Z","timestamp":460166400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1984,8]]},"DOI":"10.1007\/bf00289237","type":"journal-article","created":{"date-parts":[[2004,10,5]],"date-time":"2004-10-05T03:22:27Z","timestamp":1096946547000},"page":"125-169","source":"Crossref","is-referenced-by-count":56,"title":["An approach to automating the verification of compact parallel coordination programs. I"],"prefix":"10.1007","volume":"21","author":[{"given":"Boris D.","family":"Lubachevsky","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/S0022-0000(75)80018-3","volume":"10","author":"E.A. Ashcroft","year":"1975","unstructured":"Ashcroft, E.A.: Proving assertions about parallel programs. Journ. Comput. System Sci. 10, 110?135 (1975)","journal-title":"Journ. Comput. System Sci."},{"key":"CR2","unstructured":"Ben-Ari, M.: Temporal logic proofs of concurrent programs. Dept. Appl. Math., Weizmann Institute of Science, Report CS82-12, 1982"},{"issue":"3","key":"CR3","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1145\/357103.357109","volume":"2","author":"E.M. Clarke","year":"1980","unstructured":"Clarke, E.M.: Synthesis of resource invariants for concurrent programs. ACM Trans. on Programming Languages and Systems. 2 (3), 338?358 (1980)","journal-title":"ACM Trans. on Programming Languages and Systems."},{"key":"CR4","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1145\/362759.362813","volume":"14","author":"P.J. Courtois","year":"1971","unstructured":"Courtois, P.J., Heymans, F., Parnas, D.L.: Concurrent control with ?readers? and ?writers?. Comm. ACM 14, 667?668 (1971)","journal-title":"Comm. ACM"},{"key":"CR5","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"E.M. Dijkstra","year":"1971","unstructured":"Dijkstra, E.M.: Hierarchical orderings of sequential processes. Acta Informat. 1, 115?138 (1971)","journal-title":"Acta Informat."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0304-3975(81)90113-4","volume":"13","author":"H.J. Genrich","year":"1981","unstructured":"Genrich, H.J., Lautenbach, K.: System modeling with high-level Petri Nets. Theor. Comput. Sci. 13, 109?136 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1109\/TC.1983.1676201"},{"issue":"2","key":"CR8","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1145\/69624.357206","volume":"5","author":"A. Gottlieb","year":"1983","unstructured":"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)","journal-title":"ACM Trans, on Comput. Lang. Sys."},{"issue":"3","key":"CR9","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1145\/361268.361277","volume":"15","author":"A.N. Habermann","year":"1972","unstructured":"Habermann, A.N.: Synchronization of communicating processes. Comm. ACM. 15 (3), 171?176 (1972)","journal-title":"Comm. ACM."},{"key":"CR10","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(79)90041-0","volume":"8","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J., Pansiot, J.J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135?159 (1979)","journal-title":"Theor. Comput. Sci."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. System. Sci. 3, 147?195 (1969)","journal-title":"J. Comput. System. Sci."},{"key":"CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/BFb0022469","volume-title":"Semantics of Concurrent Computation","author":"Y.S. Kwong","year":"1979","unstructured":"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"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 125?143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"CR14","unstructured":"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"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1016\/0020-0190(79)90147-9","volume":"8","author":"J.M. Morris","year":"1979","unstructured":"Morris, J.M.: A starvation-free solution to the mutual exclusion problem. Information Processing Lett. 8, 76?80 (1979)","journal-title":"Information Processing Lett."},{"issue":"No. 5","key":"CR16","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, No. 5, p. 279?285 (May 1976)","journal-title":"Comm. ACM"},{"key":"CR17","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. I. Acta Informat. 6, 319?340 (1976)","journal-title":"Acta Informat."},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Prog. Lang, and Syst. 3, vol. 4 (July 1982)","DOI":"10.1145\/357172.357178"},{"key":"CR19","first-page":"59","volume-title":"Machine Intelligence","author":"D. Park","year":"1969","unstructured":"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"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput Sci. 13, 45?60 (1981)","journal-title":"Theor. Comput Sci."},{"key":"CR21","unstructured":"Rudolph, L.: Software structures for ultraparallel computings. Ph.D. Thesis, Courant Inst., NYU, 1982"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"Schwartz, J.T.: Ultracomputers. ACM Trans, on Prog. Lang. Sys. pp. 484?521 (1980)","DOI":"10.1145\/357114.357116"},{"key":"CR23","unstructured":"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"},{"key":"CR24","volume-title":"The logical design of operating systems","author":"A.C. Shaw","year":"1974","unstructured":"Shaw, A.C.: The logical design of operating systems Englwood Cliffs: Prentice-Hall, 1974"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5, 285?309","DOI":"10.2140\/pjm.1955.5.285"},{"key":"CR26","unstructured":"Thau, R.: Private communication."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00264015","volume":"12","author":"A. Lamsweerde van","year":"1979","unstructured":"van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct concurrent programs. Acta Informat. 12, 1?31 (1979)","journal-title":"Acta Informat."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00289237.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00289237\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00289237","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T08:09:58Z","timestamp":1585901398000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00289237"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984,8]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1984,8]]}},"alternative-id":["BF00289237"],"URL":"https:\/\/doi.org\/10.1007\/bf00289237","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1984,8]]}}}