{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:31:44Z","timestamp":1759991504315},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540347507"},{"type":"electronic","value":"9783540347521"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11768173_8","type":"book-chapter","created":{"date-parts":[[2006,6,21]],"date-time":"2006-06-21T12:02:49Z","timestamp":1150891369000},"page":"123-140","source":"Crossref","is-referenced-by-count":18,"title":["Unifying Theories in ProofPower-Z"],"prefix":"10.1007","author":[{"given":"Marcel","family":"Oliveira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"ProofPower, At: http:\/\/www.lemma-one.com\/ProofPower\/index\/index.html"},{"issue":"2\u20133","key":"8_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"},{"key":"8_CR3","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.L.C. Cavalcanti","year":"2006","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: 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)"},{"key":"8_CR4","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P.: Angelic nondeterminism and Unifying Theories of Programming. Technical Report 13-04, Computing Laboratory, University of Kent (June 2004)"},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-0-387-35261-9_29","volume-title":"Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997)","author":"C. Fischer","year":"1997","unstructured":"Fischer, C.: CSP-OZ:\u00a0A combination of Object-Z and CSP. In: Bowmann, H., Derrick, J. (eds.) Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol.\u00a02, pp. 423\u2013438. Chapman and Hall, Boca Raton (1997)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF. In: Gordon, M., Wadsworth, C.P., Milner, R. (eds.) Edinburgh LCF. LNCS, vol.\u00a078, Springer, Heidelberg (1979)"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","key":"8_CR7","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"8_CR8","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":"8_CR9","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, Englewood Cliffs (1998)"},{"key":"8_CR10","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Nuka, G., Woodcock, J.C.P.: Mechanising the alphabetised relational calculus. In: WMF 2003: 6th Braziliam Workshop on Formal Methods, Campina Grande, Brazil, vol.\u00a095, pp. 209\u2013225 (October 2004)","DOI":"10.1016\/j.entcs.2004.04.013"},{"key":"8_CR12","unstructured":"Oliveira, M.V.M.: Formal Derivation of State-Rich Reactive Programs using Circus \u2013 Additional Material (2006), At: http:\/\/www.cs.york.ac.uk\/circus\/refinement-calculus\/oliveira-phd\/"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-540-30482-1_29","volume-title":"Formal Methods and Software Engineering","author":"M.V.M. Oliveira","year":"2004","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C.: From Circus to JCSP. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 320\u2013340. Springer, Heidelberg (2004)"},{"key":"8_CR14","series-title":"Concurrent Systems Engineering Series","first-page":"281","volume-title":"Communicating Process Architectures","author":"M.V.M. Oliveira","year":"2004","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Refining industrial scale systems in Circus. In: East, I., Martin, J., Welch, P., Duce, D., Green, M. (eds.) Communicating Process Architectures. Concurrent Systems Engineering Series, vol.\u00a062, pp. 281\u2013309. IOS Press, Amsterdam (2004)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-45236-2_19","volume-title":"FME 2003: Formal Methods","author":"S.C. Qin","year":"2003","unstructured":"Qin, S.C., Dong, J.S., Chin, W.N.: A semantic foundation of TCOZ in Unifying Theories of Programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 321\u2013340. Springer, Heidelberg (2003)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","first-page":"33","volume-title":"Computer Security - ESORICS 94","author":"A.W. Roscoe","year":"1994","unstructured":"Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through Determinism. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol.\u00a0875, pp. 33\u201354. Springer, Heidelberg (1994)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES System. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 72\u201385. Springer, Heidelberg (1997)"},{"key":"8_CR18","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":"8_CR19","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1109\/ICFEM.1997.630435","volume-title":"International Conference on Formal Engineering Methods","author":"K. Taguchi","year":"1997","unstructured":"Taguchi, K., Araki, K.: The state-based CCS semantics for concurrent Z specification. In: Hinchey, M., Liu, S. (eds.) International Conference on Formal Engineering Methods, pp. 283\u2013292. IEEE, Los Alamitos (1997)"},{"key":"8_CR20","first-page":"437","volume-title":"Proceedings of the 1st International Conference on Integrated Formal Methods","author":"H. Treharne","year":"1999","unstructured":"Treharne, H., Schneider, S.: Using a process algebra to control B operations. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proceedings of the 1st International Conference on Integrated Formal Methods, pp. 437\u2013456. Springer, Heidelberg (1999)"},{"key":"8_CR21","unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C.: Circus: a concurrent refinement language. Technical report, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford OX1 3QD UK (July 2001)"},{"key":"8_CR22","volume-title":"Using Z\u2014Specification, Refinement, and Proof","author":"J.C.P. Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z\u2014Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-36103-0_5","volume-title":"Formal Methods and Software Engineering","author":"J.C.P. Woodcock","year":"2002","unstructured":"Woodcock, J.C.P., Hughes, A.: Unifying Theories of Parallel Programming. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol.\u00a02495, pp. 24\u201337. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11768173_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:12:51Z","timestamp":1619507571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11768173_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540347507","9783540347521"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11768173_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}