{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:41Z","timestamp":1755217781610,"version":"3.43.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2002,1]]},"DOI":"10.1023\/a:1012952311559","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T10:14:19Z","timestamp":1040638459000},"page":"7-21","source":"Crossref","is-referenced-by-count":7,"title":["An Experiment in Program Composition and Proof"],"prefix":"10.1007","volume":"20","author":[{"given":"K. Mani","family":"Chandy","sequence":"first","affiliation":[]},{"given":"Michel","family":"Charpentier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"J.-R. Abrial, The B-Book: Assigning Programs to Meanings, Cambridge University Press, 1996.","key":"386593_CR1","DOI":"10.1017\/CBO9780511624162"},{"doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1988.","key":"386593_CR2","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"386593_CR3","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0167-6423(94)00033-B","volume":"24","author":"K.M. Chandy","year":"1995","unstructured":"K.M. Chandy and B.A. Sanders, \u201cPredicate transformers for reasoning about concurrent computation,\u201d Science of Computer Programming, Vol. 24, pp. 129-148, 1995.","journal-title":"Science of Computer Programming"},{"unstructured":"K.M. Chandy and B.A. Sanders, \u201cReasoning about program composition,\u201d Technical Report 96-035, University of Florida, Department of Computer and Information Science and Engineering, 1996.","key":"386593_CR4"},{"key":"386593_CR5","volume-title":"Assistance \u00e0 la R\u00e9partition de Syst\u00e8mes R\u00e9actifs","author":"M. Charpentier","year":"1997","unstructured":"M. Charpentier, \u201cAssistance \u00e0 la R\u00e9partition de Syst\u00e8mes R\u00e9actifs,\u201d PhD Thesis, Institut National Polytechnique de Toulouse, France, Nov. 1997."},{"doi-asserted-by":"crossref","unstructured":"M. Charpentier and K.M. Chandy, \u201cTowards a compositional approach to the design and verification of distributed systems,\u201d Technical Report CS-TR-99-02, California Institute of Technology, Jan. 1999, pp. 29.","key":"386593_CR6","DOI":"10.21236\/ADA451478"},{"doi-asserted-by":"crossref","unstructured":"M. Charpentier and K.M. Chandy, \u201cExamples of program composition illustrating the use of universal properties,\u201d in J. Rolim (Ed.), International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA'99), Lecture Notes in Computer Science, Vol. 1586, Springer-Verlag, April 1999, pp. 1215-1227.","key":"386593_CR7","DOI":"10.1007\/BFb0098004"},{"doi-asserted-by":"crossref","unstructured":"M. Charpentier, M. Filali, P. Mauran, G. Padiou, and P. Qu\u00e9innec, \u201cTailoring UNITY to distributed program design,\u201d in J. Rolim (Ed.), International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA'98), Lecture Notes in Computer Science, Vol. 1388, Springer-Verlag, April 1998, pp. 820-832.","key":"386593_CR8","DOI":"10.1007\/3-540-64359-1_745"},{"issue":"3","key":"386593_CR9","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long, \u201cModel checking and modular verification,\u201d ACMTransactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 843-871, 1994.","journal-title":"ACMTransactions on Programming Languages and Systems"},{"issue":"3","key":"386593_CR10","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport, \u201cThe temporal togic of actions,\u201d ACM Transactions on Programming Languages and Systems, Vol. 16, No. 3, pp. 872-923, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992.","key":"386593_CR11","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"2","key":"386593_CR12","first-page":"273","volume":"3","author":"J. Misra","year":"1995","unstructured":"J. Misra, \u201cA logic for concurrent programming: Progress,\u201d Journal of Computer and Software Engineering, Vol. 3, No. 2, pp. 273-300, 1995.","journal-title":"Journal of Computer and Software Engineering"},{"issue":"2","key":"386593_CR13","first-page":"239","volume":"3","author":"J. Misra","year":"1995","unstructured":"J. Misra, \u201cA logic for concurrent programming: Safety,\u201d Journal of Computer and Software Engineering, Vol. 3, No. 2, pp. 239-272, 1995.","journal-title":"Journal of Computer and Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"C. Morgan, P. Gardiner, K. Robinson, and T. Vickers, On the Refinement Calculus, FACIT, Springer-Verlag, 1994.","key":"386593_CR14","DOI":"10.1007\/978-1-4471-3273-8"},{"issue":"2","key":"386593_CR15","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF01898402","volume":"3","author":"B.A. Sanders","year":"1991","unstructured":"B.A. Sanders, \u201cEliminating the substitution axiom from UNITY logic,\u201d Formal Aspects of Computing, Vol. 3, No. 2, pp. 189-205, 1991.","journal-title":"Formal Aspects of Computing"},{"issue":"3","key":"386593_CR16","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/158439.158441","volume":"25","author":"A.U. Shankar","year":"1993","unstructured":"A.U. Shankar, \u201cAn introduction to assertional reasoning for concurrent systems,\u201d ACM Computing Surveys, Vol. 25, No. 3, pp. 225-262, 1993.","journal-title":"ACM Computing Surveys"},{"key":"386593_CR17","volume-title":"A Method for the Specification, Composition, and Testing of Distributed Object Systems","author":"P.A.G. Sivilotti","year":"1997","unstructured":"P.A.G. Sivilotti, \u201cA Method for the Specification, Composition, and Testing of Distributed Object Systems,\u201d PhD Thesis, California Institute of Technology, 256-80 Caltech, Pasadena, California 91125, Dec. 1997."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1012952311559.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1012952311559\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1012952311559.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T20:04:07Z","timestamp":1754424247000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1012952311559"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,1]]}},"alternative-id":["386593"],"URL":"https:\/\/doi.org\/10.1023\/a:1012952311559","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2002,1]]}}}