{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:24:03Z","timestamp":1694622243314},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2002,8,1]],"date-time":"2002-08-01T00:00:00Z","timestamp":1028160000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2002,8]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>One way to reason about parallel processes is to assume that the execution of each process is subdivided into \u2018small enough\u2019 steps, and that these are executed in an interleaved fashion, thus obtaining a sequential program. The steps should be so small that for any parallel execution there will, in a suitable sense, exist a corresponding interleaved execution ending in the same state. The usual way to ensure this is to require that each step should contain at most one global access. However, if the global entities are communication channels, then larger steps may in some cases be allowed, and this may make reasoning about the programs easier. This paper explores these cases, and discusses consequences or verification and deadlock avoidance.<\/jats:p>","DOI":"10.1007\/s001650200023","type":"journal-article","created":{"date-parts":[[2003,12,10]],"date-time":"2003-12-10T21:38:13Z","timestamp":1071092293000},"page":"471-492","source":"Crossref","is-referenced-by-count":0,"title":["On Verification of Parallel Message-Passing Processes"],"prefix":"10.1145","volume":"13","author":[{"given":"Stein","family":"Krogdahl","sequence":"first","affiliation":[{"name":"Department of Informatics,University of Oslo, Norway, , , , , , NO"}]},{"given":"Olav","family":"Lysne","sequence":"additional","affiliation":[{"name":"Simula Research Laboratory, Oslo, Norway, , , , , , NO"}]}],"member":"320","reference":[{"issue":"1","key":"p_1","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/214451.214456","article-title":"Distributed snapshots: determining global states of distributed systems","volume":"3","author":"Chandy K.","year":"1985","journal-title":"ACM Transactions on Computer Systems"},{"key":"p_2","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/0020-0190(90)90027-U","article-title":"Comments on `On the proof of a distributed algorithm': always-true is not invariant","volume":"35","author":"Van Gasteren A. J. M.","year":"1990","journal-title":"Information Processing Letters"},{"issue":"12","key":"p_3","doi-asserted-by":"crossref","first-page":"1323","DOI":"10.1109\/71.553309","article-title":"Detection of strong unstable predicates in distributed systems","volume":"7","author":"Garg V. K.","year":"1996","journal-title":"IEEE Transactions on Parallel and Distributed Programs"},{"key":"p_4","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/BF01212527","article-title":"Verifying a distributed list system: A case history","volume":"9","author":"Krogdahl S.","year":"1997","journal-title":"Formal Aspects of Computing"},{"key":"p_5","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/BF01932022","article-title":"Verification of a class of link-level protocols","volume":"18","author":"Krogdahl S.","year":"1978","journal-title":"BIT"},{"key":"p_6","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BF00289062","article-title":"The `Hoare logic' of concurrent programs","volume":"14","author":"Lamport L.","year":"1980","journal-title":"Acta Informatica"},{"key":"p_7","first-page":"336","volume-title":"Proceedings of the 1999 International Conference of Parallel Processing","author":"Lee E.","year":"1999"},{"key":"p_9","first-page":"62","article-title":"Global conditions in debugging distributed programs","volume":"15","author":"Manabe Y.","year":"1992","journal-title":"IEEE Transactions on Parallel and Distributed Programs"},{"key":"p_10","first-page":"215","volume-title":"Proceedings of the 5th International Workshop on Parallel and Distributed Algorithms","author":"Marzullo K.","year":"1991"},{"key":"p_11","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/BF01211310","article-title":"Axiomatic treatment of processes with shared variables revisited","volume":"4","author":"Owe O.","year":"1992","journal-title":"Formal Aspects of Computing"},{"key":"p_12","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0167-6423(95)00002-A","article-title":"Verifying programs that use causally-ordered message-passing","volume":"24","author":"Stoller S. D.","year":"1995","journal-title":"Science of Computer Programming"},{"issue":"2","key":"p_13","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1109\/32.345831","article-title":"Testing and debugging distributed programs using global predicates","volume":"21","author":"Venkatesan S.","year":"1995","journal-title":"IEEE Transactions on Software Engineering"},{"key":"p_14","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0020-0190(87)90123-2","article-title":"On the proof of a distributed algorithm","volume":"25","author":"Verjus J. P.","year":"1987","journal-title":"Information Processing Letters"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650200023.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650200023\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650200023","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:34:07Z","timestamp":1641483247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650200023"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,8]]},"references-count":13,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2002,8]]}},"alternative-id":["10.1007\/s001650200023"],"URL":"https:\/\/doi.org\/10.1007\/s001650200023","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,8]]}}}