{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:25Z","timestamp":1725664165323},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540606888"},{"type":"electronic","value":"9783540492627"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60688-2_58","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:52:31Z","timestamp":1330289551000},"page":"396-410","source":"Crossref","is-referenced-by-count":0,"title":["ESP-MC: An experiment in the use of verification tools"],"prefix":"10.1007","author":[{"given":"Xiaojun","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paola","family":"Inverardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo","family":"Montangero","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"V. Ambriola, P. Ciancarini, and C. Montangero. Software process enactment in Oikos. In R. N. Taylor, editor, Proc. of ACM SIGSOFT '90, ACM Soft. Eng. Notes 15(6), Dec. 1990.","DOI":"10.1145\/99277.99294"},{"key":"29_CR2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-17660-8_55","volume":"249","author":"E. Astesiano","year":"1987","unstructured":"E. Astesiano and G. Reggio. SMoLCS-Driven concurrent calculi. Lecture Notes in Computer Science, 249:169\u2013201, 1987.","journal-title":"Lecture Notes in Computer Science"},{"issue":"1\/3","key":"29_CR3","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"J.A. Bergstra","year":"1984","unstructured":"J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60(1\/3):109\u2013137, 1984.","journal-title":"Information and Control"},{"key":"29_CR4","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structure in propositional temporal logic. Theoretical Computer Science, 59:115\u2013131, 1988.","journal-title":"Theoretical Computer Science"},{"key":"29_CR5","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-55253-7_6","volume":"582","author":"X. J. Chen","year":"1992","unstructured":"X. J. Chen and C. Montangero. Compositional refinements of multiple blackboard systems. Lecture Notes in Computer Science, 582:93\u2013109, 1992.","journal-title":"Lecture Notes in Computer Science"},{"key":"29_CR6","first-page":"5","volume":"32","author":"X. J. Chen","year":"1995","unstructured":"X. J. Chen and C. Montangero. Compositional refinements of multiple blackboard systems. Acta Informatica, 32:5, 1995.","journal-title":"Acta Informatica"},{"issue":"2","key":"29_CR7","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specification. ACM TOPLAS, 8(2):244\u2013263, 1986.","journal-title":"ACM TOPLAS"},{"key":"29_CR8","unstructured":"R. de Simone and D. Vergamini. Aboard AUTO. Technical Report 111, INRIA, 1989."},{"issue":"1","key":"29_CR9","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. \u201cSometimes\u201d and \u201cNot Never\u201d revisited: on branching time versus linear time temporal logic. Journal of ACM, 33(1):151\u2013178, 1986.","journal-title":"Journal of ACM"},{"key":"29_CR10","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BFb0013022","volume":"354","author":"E.A. Emerson","year":"1989","unstructured":"E.A. Emerson and J. Srinivasan. Branching time temporal logic. Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS, 354:123\u2013172, 1989.","journal-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS"},{"key":"29_CR11","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall Int., London, 1985."},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"B. Jonsson and J. Parrow. Deciding bisimulation equivalences for a class of nonfinte-state programs. In Proc. 6th Symposium on Theoretical Aspects of Computer Science, LNCS 349, pages 421\u2013433. Springer-Verlag, 1989.","DOI":"10.1007\/BFb0029004"},{"key":"29_CR13","first-page":"110","volume":"47","author":"E. Madelaine","year":"1992","unstructured":"E. Madelaine. Verification tools for the concur project. Bull. EATCS, 47:110\u2013120, 1992.","journal-title":"Bull. EATCS"},{"key":"29_CR14","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, London, 1989."},{"issue":"7","key":"29_CR15","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","volume":"25","author":"R. Nicola De","year":"1993","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi, and G. Ristori. An action based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems, 25(7):761\u2013778, Feb. 1993.","journal-title":"Computer Networks and ISDN Systems"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"R. De Nicola and F. Vaandrager. Action versus state based logics for transition systems. Proceedings Ecole de Printemps on Semantics of Concurrency, LNCS, 469, 1990.","DOI":"10.1007\/3-540-53479-2_17"},{"key":"29_CR17","unstructured":"G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981."},{"key":"29_CR18","unstructured":"V. Roy and R. de Simone. An AUTOGRAPH primer. Technical Report 112, I.N.R.I.A., 1989."}],"container-title":["Lecture Notes in Computer Science","Algorithms, Concurrency and Knowledge"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60688-2_58.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:01:17Z","timestamp":1605646877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60688-2_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540606888","9783540492627"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-60688-2_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}