{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T23:26:19Z","timestamp":1725578779772},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642198281"},{"type":"electronic","value":"9783642198298"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-19829-8_18","type":"book-chapter","created":{"date-parts":[[2011,3,16]],"date-time":"2011-03-16T10:20:41Z","timestamp":1300270841000},"page":"274-290","source":"Crossref","is-referenced-by-count":2,"title":["Automating Refinement of Circus Programs"],"prefix":"10.1007","author":[{"given":"Frank","family":"Zeyda","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Butterfield, A.: Saoith\u00edn Proof Assistant, \n                  \n                    http:\/\/www.scss.tcd.ie\/Andrew.Butterfield\/Saoithin\/"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/11526841_18","volume-title":"FM 2005:\u00a0Formal Methods","author":"A. Cavalcanti","year":"2005","unstructured":"Cavalcanti, A., Clayton, P., O\u2019Halloran, C.: Control Law Diagrams in Circus. In: FM 2005:\u00a0Formal Methods. LNCS, vol.\u00a03582, pp. 253\u2013268. Springer, Heidelberg (2005)"},{"key":"18_CR3","unstructured":"Cavalcanti, A., Clayton, P., O\u2019Halloran, C.: From Control Law Diagrams to Ada via Circus. Technical report, University of York, York, U.K. (April 2008)"},{"issue":"2-3","key":"18_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":"18_CR5","series-title":"Prentice Hall Series in Automatic Computation","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice Hall Series in Automatic Computation. Prentice Hall, Englewood Cliffs (1976)"},{"key":"18_CR6","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)"},{"issue":"4","key":"18_CR7","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/BF01213535","volume":"8","author":"A. Martin","year":"1996","unstructured":"Martin, A., Gardiner, P., Woodcock, J.: A Tactic Calculus - Abridged Version. Formal Aspects of Computing\u00a08(4), 479\u2013489 (1996)","journal-title":"Formal Aspects of Computing"},{"key":"18_CR8","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":"18_CR9","unstructured":"Oliveira, M.: Formal Derivation of State-Rich Reactive Programs using Circus. PhD thesis, Department of Computer Science, University of York (2005)"},{"key":"18_CR10","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:\u00a0a refinement tactic language for Circus. Electronic Notes in Theoretical Computer Science\u00a0214, 203\u2013229 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"18_CR11","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/s00165-003-0003-8","volume":"15","author":"M. Oliveira","year":"2003","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: ArcAngel:\u00a0a Tactic Language for Refinement. Formal Aspects of Computing\u00a015(1), 28\u201347 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects of Computing, Online First (December 2007)","DOI":"10.1007\/s00165-007-0052-5"},{"key":"18_CR13","unstructured":"Oliveira, M., Cavalcanti, A., Zeyda, F.: A Tactic Language for Refinement of State-Rich Concurrent Specifications (to appear)"},{"key":"18_CR14","first-page":"310","volume-title":"Proceedings of the Second Int. Conference on Software Engineering and Formal Methods","author":"M. Oliveira","year":"2004","unstructured":"Oliveira, M., Xavier, M., Cavalcanti, A.: Refine and Gabriel:\u00a0Support for Refinement and Tactics. In: Proceedings of the Second Int. Conference on Software Engineering and Formal Methods, pp. 310\u2013319. IEEE Computer Society, Los Alamitos (2004)"},{"key":"18_CR15","series-title":"Prentice Hall Series in Computer Science","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall Series in Computer Science. Prentice Hall, Englewood Cliffs (1997)"},{"key":"18_CR16","series-title":"Prentice-Hall International Series In Computer Science","volume-title":"The Z Notation:\u00a0A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation:\u00a0A Reference Manual. Prentice-Hall International Series In Computer Science. Prentice Hall PTR, Englewood Cliffs (1992)"},{"key":"18_CR17","volume-title":"BCS FACS Sixth Refinement Workshop \u2013 Theory and Practise of Formal Software Development, London, U.K.","author":"J. Wright von","year":"1994","unstructured":"von Wright, J.: Program Refinement by Theorem Prover. In: BCS FACS Sixth Refinement Workshop \u2013 Theory and Practise of Formal Software Development, London, U.K. Springer, Heidelberg (1994)"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/j.entcs.2009.12.027","volume":"259","author":"F. Zeyda","year":"2009","unstructured":"Zeyda, F., Cavalcanti, A.: Supporting ArcAngel in ProofPower. Electronic Notes in Theoretical Computer Science\u00a0259, 225\u2013243 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Zeyda, F., Cavalcanti, A.: Mechanical Reasoning about Families of UTP Theories. Science of Computer Programming (March 2010), doi:dx.doi.org\/10.1016\/j.scico.2010.02.010","DOI":"10.1016\/j.entcs.2009.05.055"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19829-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T06:56:17Z","timestamp":1558421777000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19829-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198281","9783642198298"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19829-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}