{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T21:25:40Z","timestamp":1663795540414},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540438571","type":"print"},{"value":"9783540454427","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45442-x_14","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T00:55:08Z","timestamp":1179190508000},"page":"233-262","source":"Crossref","is-referenced-by-count":29,"title":["From Kleene Algebra to Refinement Algebra"],"prefix":"10.1007","author":[{"given":"Joakim","family":"von Wright","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,21]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"C. Aarts et al. Fixpoint calculus. Information Processing Letters, 53(3), February 1995.","DOI":"10.1016\/0020-0190(94)00195-5"},{"issue":"5","key":"14_CR2","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s001650070008","volume":"12","author":"R. J. Back","year":"2000","unstructured":"R. J. Back and J. von Wright. Encoding, decoding, and data refinement. Formal Aspects of Computing, 12(5):313\u2013349, 2000.","journal-title":"Formal Aspects of Computing"},{"key":"14_CR3","series-title":"Mathematical Centre Tracts","volume-title":"Correctness Preserving Program Refinements: Proof Theory and Applications","author":"R.J. Back","year":"1980","unstructured":"R.J. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Centre Tracts. Mathematical Centre, Amsterdam, 1980."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"R.J. Back. Refining atomicity in parallel algorithms. In PARLE Conference on Parallel Architectures and Languages Europe, Eindhoven, the Netherlands, June 1989. Springer-Verlag.","DOI":"10.1007\/3-540-51285-3_42"},{"key":"14_CR5","first-page":"17","volume":"12","author":"R.J. Back","year":"1991","unstructured":"R.J. Back and K. Sere. Stepwise refinement of action systems. Structured Programming, 12:17\u201330, 1991.","journal-title":"Structured Programming"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"R.J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s002360050163","volume":"36","author":"R.J. Back","year":"1999","unstructured":"R.J. Back and J. von Wright. Reasoning algebraically about loops. Acta Informatica, 36:295\u2013334, 1999.","journal-title":"Acta Informatica"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1093\/imamat\/15.2.161","volume":"15","author":"R.C. Backhouse","year":"1975","unstructured":"R.C. Backhouse and B.A. Carr\u00e9. Regular algebra applied to path finding problems. Journal Inst. Math. Appl., 15:161\u2013186, 1975.","journal-title":"Journal Inst. Math. Appl."},{"key":"14_CR9","unstructured":"J.W. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall, 1980."},{"key":"14_CR10","unstructured":"W. Chen and J.T. Udding. Program inversion: more than fun! Report CS 8903, Department of Mathematics and Computer Science, University of Groningen, 1988."},{"key":"14_CR11","unstructured":"E. Cohen. Hypotheses in Kleene Algebra. Unpublished manuscript, Telcordia, 1994."},{"key":"14_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"E. Cohen. Separation and reduction. In Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, Portugal, July 2000. Springer-Verlag."},{"key":"14_CR13","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976."},{"key":"14_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0167-6423(99)00021-0","volume":"37","author":"R.M. Dijkstra","year":"2000","unstructured":"R.M. Dijkstra. Computation calculus bridging a formalization gap. Science of Computer Programming, 37:3\u201336, 2000.","journal-title":"Science of Computer Programming"},{"key":"14_CR15","doi-asserted-by":"crossref","volume-title":"The Science of Programming","author":"D. Gries","year":"1981","unstructured":"D. Gries. The Science of Programming. Springer-Verlag, New York, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"14_CR16","unstructured":"I.J. Hayes. Reasoning about real-time repetitions: Terminating and nonterminating. Techn. Rep. 01-04, Software Verification Research Centre, The University of Queensland, February 2001."},{"issue":"3","key":"14_CR17","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1999","unstructured":"D. Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 19(3):427\u2013443, 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"14_CR18","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","unstructured":"D. Kozen. On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic, 1(1):60\u201376, 2000.","journal-title":"ACM Transactions on Computational Logic"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"D. Kozen and M-C. Patron. Certification of compiler optimizations using Kleene Algebra with tests. In 1st International Conference on Computational logic, volume 1861 of Lecture Notes in Artificial Intelligence, pages 568\u2013582, London, July 2000. Springer-Verlag.","DOI":"10.1007\/3-540-44957-4_38"},{"key":"14_CR20","unstructured":"M.S. Manasse and C.G. Nelson. Correct compilation of control structures. Techn. Memo. 11271-840909-09\u2122, AT&T Bell Laboratories, September 1984."},{"key":"14_CR21","unstructured":"C.C. Morgan. Programming from Specifications. Prentice-Hall, 1990."},{"key":"14_CR22","unstructured":"J.L.A. van de Snepscheut. On lattice theory and program semantics. Technical Report CS-TR-93-19, Caltech, Pasadena, California, USA, 1993."},{"issue":"2","key":"14_CR23","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0020-0190(91)90141-4","volume":"37","author":"J. Wright","year":"1991","unstructured":"J. von Wright. Program inversion in the refinement calculus. Information Processing Letters, 37(2):95\u2013100, January 1991.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45442-X_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:21:46Z","timestamp":1556396506000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45442-X_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540438571","9783540454427"],"references-count":23,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-45442-x_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"published":{"date-parts":[[2002]]}}}