{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:34:40Z","timestamp":1759991680884},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642145209"},{"type":"electronic","value":"9783642145216"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14521-6_13","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T10:52:24Z","timestamp":1280400744000},"page":"218-237","source":"Crossref","is-referenced-by-count":7,"title":["Encoding Circus Programs in ProofPowerZ"],"prefix":"10.1007","author":[{"given":"Frank","family":"Zeyda","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/11576280_32","volume-title":"Formal Methods and Software Engineering","author":"M. Adams","year":"2005","unstructured":"Adams, M., Clayton, P.: ClawZ: Cost-Effective Formal Verification of Control Systems. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 465\u2013479. Springer, Heidelberg (2005)"},{"key":"13_CR2","unstructured":"Camilleri, A.: A Higher Order Logic Mechanisation of the CSP Failure-Divergence Semantics. Technical Report HPL-90-194, HP Laboratories (September 1990)"},{"issue":"9","key":"13_CR3","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/32.58786","volume":"16","author":"A. Camilleri","year":"1990","unstructured":"Camilleri, A.: Mechanizing csp trace theory in higher order logic. IEEE Transactions on Software Engeneering\u00a016(9), 993\u20131004 (1990)","journal-title":"IEEE Transactions on Software Engeneering"},{"issue":"2-3","key":"13_CR4","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"A. Cavalcanti","year":"2003","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: A Refinement Strategy for Circus. Formal Aspects of Computing\u00a015(2-3), 146\u2013181 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0028390","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1997","unstructured":"Dutertre, B., Schneider, S.: Using a PVS embedding of CSP to verify authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 121\u2013136. Springer, Heidelberg (1997)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1007\/11901433_38","volume-title":"Formal Methods and Software Engineering","author":"L. Freitas","year":"2006","unstructured":"Freitas, L., Cavalcanti, A., Woodcock, J.: Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 697\u2013716. Springer, Heidelberg (2006)"},{"key":"13_CR7","unstructured":"Freitas, L., Woodcock, J., Cavalcanti, A.: An Architecture for Circus Tools. In: SBMF 2007:\u00a0Brazilian Symp. on Formal Methods, August 2007, pp. 6\u201321 (2007)"},{"key":"13_CR8","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-1-4471-3550-0_14","volume-title":"5th Refinement Workshop","author":"L. Groves","year":"1992","unstructured":"Groves, L., Nickson, R., Utting, M.: A Tactic Driven Refinement Tool. In: 5th Refinement Workshop, January 1992, pp. 272\u2013297. Springer, Heidelberg (1992)"},{"key":"13_CR9","series-title":"Prentice Hall Series in Computer Science","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall, Englewood Cliffs (1998)"},{"key":"13_CR10","series-title":"Prentice-Hall International Series In Computer Science","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1998","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall International Series In Computer Science. Prentice Hall, Englewood Cliffs (1998)"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.entcs.2004.04.013","volume":"95","author":"G. Nuka","year":"2004","unstructured":"Nuka, G., Woodcock, J.: Mechanising the Alphabetised Relational Calculus. Electronic Notes in Theoretical Computer Science\u00a095, 209\u2013225 (2004)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/11768173_13","volume-title":"Unifying Theories of Programming","author":"G. Nuka","year":"2006","unstructured":"Nuka, G., Woodcock, J.: Mechanising a Unifying Theory. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol.\u00a04010, pp. 217\u2013235. Springer, Heidelberg (2006)"},{"key":"13_CR13","unstructured":"Oliveira, M.: Formal Derivation of State-Rich Reactive Programs using Circus. PhD thesis, Department of Computer Science, University of York, UK (2005)"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.entcs.2008.06.010","volume":"214","author":"M. Oliveira","year":"2008","unstructured":"Oliveira, M., Cavalcanti, A.: ArcAngelC: a Refinement Tactic Language for Circus. Electronic Notes in Theoretical Computer Science\u00a0214, 203\u2013229 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11768173_8","volume-title":"Unifying Theories of Programming","author":"M. Oliveira","year":"2006","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying Theories in ProofPower-Z. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol.\u00a04010, pp. 123\u2013140. Springer, Heidelberg (2006)"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects of Computing (2007) (Online First)","DOI":"10.1007\/s00165-007-0052-5"},{"key":"13_CR17","unstructured":"Xavier, M., Cavalcanti, A., Sampaio, A.: Type Checking Circus Specifications. In: SBMF 2006:\u00a0Brazilian Symposium on Formal Methods, pp. 105\u2013120 (2006)"},{"key":"13_CR18","unstructured":"Zeyda, F., Cavalcanti, A.: Mechanical Reasoning about Families of UTP Theories. In: SBMF 2008:\u00a0Brazilian Symp. on Formal Methods, pp. 145\u2013160 (2008)"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14521-6_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:54:24Z","timestamp":1606186464000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14521-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642145209","9783642145216"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14521-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}