{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:53:41Z","timestamp":1762458821587},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540278825"},{"type":"electronic","value":"9783540317142"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11526841_17","type":"book-chapter","created":{"date-parts":[[2010,7,18]],"date-time":"2010-07-18T16:51:58Z","timestamp":1279471918000},"page":"237-252","source":"Crossref","is-referenced-by-count":11,"title":["Operational Semantics for Model Checking Circus"],"prefix":"10.1007","author":[{"given":"Jim","family":"Woodcock","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"given":"Leonardo","family":"Freitas","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: Refinement of actions in Circus. In: REFINE 2002. Electronic Notes in Theor. Comp. Sci., vol.\u00a070(3) (2002)","DOI":"10.1016\/S1571-0661(05)80489-X"},{"issue":"2\u20133","key":"17_CR2","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"A.L.C. Cavalcanti","year":"2003","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Formal Aspects of Computing\u00a015(2\u20133), 146\u2013181 (2003)","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"17_CR3","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1049\/ip-sen:20030131","volume":"150","author":"A.L.C. Cavalcanti","year":"2003","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: Predicate transformers in the semantics of Circus. IEE Proceedings Software\u00a0150(2), 85\u201394 (2003)","journal-title":"IEE Proceedings Software"},{"key":"17_CR4","unstructured":"Fischer, C.: Combining CSP and Z.Technical Report. Univ. Oldenburg (1996)"},{"key":"17_CR5","unstructured":"Goldsmith, M.: FDR2 User\u2019s Manual version 2.67. FSEL (May 2000)"},{"key":"17_CR6","unstructured":"Jifeng, H., Liu, Z., Li, X.: A Relational Model for Object-Oriented Programming. Tech. Rep. 231. UNU\/IIST, P.\u00a0O.\u00a0Box 3058, Macau (May 2001)"},{"key":"17_CR7","first-page":"69","volume-title":"Procs ICCI 2002","author":"H. Jifeng","year":"2002","unstructured":"Jifeng, H., Liu, Z., Li, X.: Towards a Refinement Calculus for Object Systems. In: Procs ICCI 2002, pp. 69\u201377. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"17_CR8","unstructured":"Jifeng, H., Liu, Z., Li, X.: Modelling Object-oriented Programming with Reference Type and Dynamic Binding. Tech. Rep. 280. UNU\/IIST (2003)"},{"key":"17_CR9","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"17_CR10","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)"},{"key":"17_CR11","unstructured":"Information Technology \u2014 Z Formal Specification Notation \u2014 Syntax, Type System and Semantics. ISO\/IEC 13568 (2002)"},{"key":"17_CR12","unstructured":"Lemma-One. ProofPower Tutorial (2003)"},{"key":"17_CR13","volume-title":"Commun. Proc. Archs.","author":"M. Jeremy","year":"2000","unstructured":"Jeremy, M., Martin, R., Huddart, Y.: Parallel Algorithms for Deadlock and Livelock Analysis of Concurrent Systems. In: Commun. Proc. Archs. IOS Press, Amsterdam (2000)"},{"key":"17_CR14","unstructured":"Meisels, I., Saaltink, M.: Z\/Eves 1.5 Reference Manual. Technical Report TR-97-5493-03d. ORA Canada (September 1997)"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Nuka, G., Woodcock, J.: Mechanising the alphabetised relational calculus. In: WMF2003. Electronic Notes in Theoretical Computer Science, vol.\u00a095 (2004)","DOI":"10.1016\/j.entcs.2004.04.013"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying theories in ProofPowerZ. Draft. University of York (January 2005)","DOI":"10.1007\/11768173_8"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.jlap.2004.03.009","volume":"60\/61","author":"G.D. Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A Structural approach to Operational Semantics. Journal of Logic and Algebraic Programming\u00a060\/61, 19\u2013140 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"17_CR18","unstructured":"ProBE User\u2019s Manual version 1.28. Formal Systems (Europe) Ltd. (May 2000)"},{"key":"17_CR19","unstructured":"Roscoe, A.W.: Model Checking CSP. In: [20], Ch.\u00a021, pp. 353\u2013378 (1994)"},{"key":"17_CR20","volume-title":"A Classsical Mind:\u00a0Essays for C.A.R.\u00a0Hoare.","author":"A.W. Roscoe","year":"1994","unstructured":"Roscoe, A.W.: A Classsical Mind:\u00a0Essays for C.A.R.\u00a0Hoare. Prentice Hall, Englewood Cliffs (1994)"},{"key":"17_CR21","volume-title":"Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1997)"},{"key":"17_CR22","unstructured":"Saaltink, M.: Z\/Eves 2.0 User\u2019s Guide. Technical Report TR-99-5493-06a. ORA Canada (1999)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/3-540-45614-7_26","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"A.C.A. Sampaio","year":"2002","unstructured":"Sampaio, A.C.A., Woodcock, J.C.P., Cavalcanti, A.L.C.: Refinement in Circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 451\u2013470. Springer, Heidelberg (2002)"},{"key":"17_CR24","unstructured":"Scattergood, B.: The Semantics and Implementation of Machine Readable CSP. PhD thesis. Oxford University (1998)"},{"key":"17_CR25","volume-title":"Concurrent and Real-Time Systems:\u00a0The CSP Approach","author":"S. Schneider","year":"2000","unstructured":"Schneider, S.: Concurrent and Real-Time Systems:\u00a0The CSP Approach. Wiley, Chichester (2000)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-45648-1_22","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"S. Schneider","year":"2002","unstructured":"Schneider, S., Treharne, H.: Communicating B Machines. In: Bert, D., et al. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 415\u2013435. Springer, Heidelberg (2002)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1007\/3-540-36103-0_62","volume-title":"Formal Methods and Software Engineering","author":"A. Sherif","year":"2002","unstructured":"Sherif, A., Jifeng, H.: Towards a time model for circus. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol.\u00a02495, pp. 613\u2013624. Springer, Heidelberg (2002)"},{"key":"17_CR28","volume-title":"SEFM 2004","author":"X. Tang","year":"2004","unstructured":"Tang, X., Woodcock, J.: Towards mobile processes in unifying theories. In: SEFM 2004. IEEE Computer Society, Los Alamitos (2004)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-27764-4_20","volume-title":"Mathematics of Program Construction","author":"X. Tang","year":"2004","unstructured":"Tang, X., Woodcock, J.: Travelling processes. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 381\u2013399. Springer, Heidelberg (2004)"},{"key":"17_CR30","volume-title":"Logic and Algebra for Engineering Software","author":"J.C.P. Woodcock","year":"2002","unstructured":"Woodcock, J.C.P.: Unifying Theories of Parallel Programming. In: Logic and Algebra for Engineering Software. IOS Press, Amsterdam (2002)"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Cavalcanti, A.: A Concurrent Language for Refinement. In: 5th Irish Workshop on Formal Methods (2001)","DOI":"10.14236\/ewic\/IWFM2001.7"},{"key":"17_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J. Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The semantics of circus. In: Bert, D., et al. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 184\u2013203. Springer, Heidelberg (2002)"},{"key":"17_CR33","volume-title":"Using Z:\u00a0Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z:\u00a0Specification, Refinement, and Proof. Prentice Hall, Englewood Cliffs (1996)"},{"key":"17_CR34","unstructured":"http:\/\/www-users.cs.york.ac.uk\/~leo"}],"container-title":["Lecture Notes in Computer Science","FM 2005: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11526841_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T18:52:07Z","timestamp":1635706327000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11526841_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540278825","9783540317142"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/11526841_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}