{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T00:47:13Z","timestamp":1649033233526},"reference-count":23,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2000,7,1]],"date-time":"2000-07-01T00:00:00Z","timestamp":962409600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4764,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2000,7]]},"DOI":"10.1016\/s0304-3975(98)00233-3","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T16:02:43Z","timestamp":1027612963000},"page":"339-361","source":"Crossref","is-referenced-by-count":6,"title":["Composing leads-to properties"],"prefix":"10.1016","volume":"243","author":[{"given":"David","family":"Meier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beverly","family":"Sanders","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(98)00233-3_BIB1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","article-title":"Composing specifications","volume":"15","author":"Abadi","year":"1993","journal-title":"ACM Trans. Program. Languages Systems"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB2","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","article-title":"Conjoining specifications","volume":"17","author":"Abadi","year":"1995","journal-title":"ACM Trans. Program. Languages Systems"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB3","series-title":"Parallel Program Design, a Foundation","author":"Chandy","year":"1988"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB4","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0167-6423(94)00033-B","article-title":"Predicate transformers for reasoning about concurrent computation","volume":"24","author":"B.A. Sanders","year":"1995","journal-title":"Sci. Computer Program."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB5","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0167-6423(94)00017-4","article-title":"Composition of assumption-commitment specifications in a UNITY style","volume":"23","author":"Colette","year":"1994","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB6","doi-asserted-by":"crossref","unstructured":"P. Colette, E. Knapp, Logical foundations for compositional verification and development of concurrent programs in UNITY, 4th Int. Conf. on Algebraic Methodology and Software Technology, 1995, Lecture Notes in Computer Science, vol. 936, Springer, Berlin, 1995.","DOI":"10.1007\/3-540-60043-4_64"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB7","series-title":"Predicate Calculus and Program Semantics","author":"Dijkstra","year":"1990"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB8","unstructured":"Foster, Olson, Tuecke, Productive parallel programming: the PCN approach, to appear in Scientific Programming."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB9","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","article-title":"Tentative steps toward a development Method for interfering programs","volume":"5","author":"Jones","year":"1983","journal-title":"ACM Trans. Program. Languages Systems"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB10","doi-asserted-by":"crossref","unstructured":"C.S. Jutla, E. Knapp, J.R. Rao, A predicate transformer approach to semantics of parallel programs, Proc. 8th ACM symp. on Principles of Distributed Computing, 1989, pp. 249\u2013263.","DOI":"10.1145\/72981.72999"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB11","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0020-0190(90)90218-M","article-title":"A predicate transformer for progress","volume":"33","author":"Knapp","year":"198990","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB12","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF02276640","article-title":"Specifying modules to satisfy interfaces \u2013 a state transition approach","volume":"6","author":"Lam","year":"1992","journal-title":"Distributed Comput."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB13","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1109\/32.263755","article-title":"A theory of interfaces and modules 1: composition theorem","volume":"20","author":"Lam","year":"1994","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB14","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1145\/361227.361234","article-title":"Reduction: a method of proving properties of parallel programs","volume":"18","author":"Lipton","year":"1975","journal-title":"Commun. ACM"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB15","unstructured":"J. Misra, A program-composition theorem involving a fixed-point, Notes on UNITY, pp. 28\u201391."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB16","doi-asserted-by":"crossref","unstructured":"J. Misra, Loosely coupled processes, Proc. PARLE\u201991, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands. Lecture Notes in Computer Science, vol. 506, Springer, Berlin, 1991, pp. 1\u201326.","DOI":"10.1007\/3-540-54152-7_55"},{"issue":"2","key":"10.1016\/S0304-3975(98)00233-3_BIB17","first-page":"239","article-title":"A logic for concurrent programming: safety","volume":"3","author":"Misra","year":"1995","journal-title":"J. Computer and Software Eng."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB18","doi-asserted-by":"crossref","unstructured":"A. Pnueli, In transition from global to modular temporal reasoning about Programs, Logics and Models of Concurrent Systems, Springer, Berlin, 1985, pp. 123\u2013144.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB19","doi-asserted-by":"crossref","unstructured":"J.R. Rao, Extensions of the unity methodology: compositionality, fairness and probability in parallelism, Lecture Notes in Computer Science, vol. 908, Springer, Berlin, 1995.","DOI":"10.1007\/3-540-59173-7"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB20","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF01898402","article-title":"Eliminating the substitution axiom from UNITY logic","volume":"3","author":"Sanders","year":"1991","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB21","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s002360050115","article-title":"Refinement of mixed specifications: a Generalization of UNITY","volume":"35","author":"Sanders","year":"1998","journal-title":"Acta Informatica"},{"key":"10.1016\/S0304-3975(98)00233-3_BIB22","unstructured":"N. Shankar, Lazy Compositional Verification, COMPOS\u201997, 1997."},{"key":"10.1016\/S0304-3975(98)00233-3_BIB23","doi-asserted-by":"crossref","unstructured":"E.W. Stark, A proof technique for rely\/guarantees properties, Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 206, Springer, Berlin, 1985, pp. 369\u2013391.","DOI":"10.1007\/3-540-16042-6_21"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397598002333?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397598002333?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,10]],"date-time":"2020-01-10T23:40:08Z","timestamp":1578699608000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397598002333"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,7]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,7]]}},"alternative-id":["S0304397598002333"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(98)00233-3","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2000,7]]}}}