{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T04:10:55Z","timestamp":1742443855227,"version":"3.40.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642277047"},{"type":"electronic","value":"9783642277054"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_20","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T17:18:06Z","timestamp":1327511886000},"page":"243-260","source":"Crossref","is-referenced-by-count":18,"title":["Isabelle\/Circus: A Process Specification and Verification Environment"],"prefix":"10.1007","author":[{"given":"Abderrahmane","family":"Feliachi","sequence":"first","affiliation":[]},{"given":"Marie-Claude","family":"Gaudel","sequence":"additional","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Andrews, P.B.: Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edn. Kluwer Academic (2002); now published by Springer","DOI":"10.1007\/978-94-015-9934-4"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Aspects of Computing (to appear, 2012)","DOI":"10.1007\/s00165-012-0222-y"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/PL00003930","volume":"12","author":"M. Butler","year":"2000","unstructured":"Butler, M.: CSP2B: A practical approach to combining CSP and B. Formal Aspects of Computing\u00a012, 182\u2013196 (2000)","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"20_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s00236-011-0133-z","volume":"48","author":"A. Cavalcanti","year":"2011","unstructured":"Cavalcanti, A., Gaudel, M.-C.: Testing for refinement in Circus. Acta Informatica\u00a048(2), 97\u2013147 (2011)","journal-title":"Acta Informatica"},{"issue":"2-3","key":"20_CR5","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-3), 146\u2013181 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11889229_6","volume-title":"Refinement Techniques in Software Engineering","author":"A. Cavalcanti","year":"2006","unstructured":"Cavalcanti, A., Woodcock, J.: A Tutorial Introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol.\u00a03167, pp. 220\u2013268. Springer, Heidelberg (2006)"},{"issue":"2","key":"20_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05(2), 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-16690-7_9","volume-title":"Unifying Theories of Programming","author":"A. Feliachi","year":"2010","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Unifying Theories in Isabelle\/HOL. In: Qin, S. (ed.) UTP 2010. LNCS, vol.\u00a06445, pp. 188\u2013206. Springer, Heidelberg (2010)"},{"key":"20_CR9","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle\/Circus : a process specification and verification environment. Technical Report 1547, Univ. Paris-Sud XI LRI (November 2011), http:\/\/www.lri.fr\/srubrique.php?news=33"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-49676-2_2","volume-title":"ZUM \u201998: The Z Formal Specification Notation","author":"C. Fischer","year":"1998","unstructured":"Fischer, C.: How to Combine Z with Process Algebra. In: Bowen, J., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol.\u00a01493, pp. 5\u201325. Springer, Heidelberg (1998)"},{"key":"20_CR11","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"20_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2006.08.047","volume":"187","author":"M. Oliveira","year":"2007","unstructured":"Oliveira, M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A denotational semantics for Circus. Electron. Notes Theor. Comput. Sci.\u00a0187, 107\u2013123 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2005.11.007","volume":"354","author":"M. Roggenbach","year":"2006","unstructured":"Roggenbach, M.: CSP-CASL: a new integration of process algebra and algebraic specification. Theor. Comput. Sci.\u00a0354, 42\u201371 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR15","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)"},{"key":"20_CR16","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. Sampaio","year":"2002","unstructured":"Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 451\u2013470. Springer, Heidelberg (2002)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Taguchi, K., Araki, K.: The state-based CCS semantics for concurrent Z specification. In: ICFEM 1997, pp. 283\u2013292. IEEE (1997)","DOI":"10.1109\/ICFEM.1997.630435"},{"key":"20_CR18","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., Bowen, J., Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 184\u2013203. Springer, Heidelberg (2002)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-14521-6_13","volume-title":"Unifying Theories of Programming","author":"F. Zeyda","year":"2010","unstructured":"Zeyda, F., Cavalcanti, A.: Encoding Circus Programs in ProofPowerZ. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol.\u00a05713, pp. 218\u2013237. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T08:19:46Z","timestamp":1742372386000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}