{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:52:24Z","timestamp":1725483144846},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"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":[[1999]]},"DOI":"10.1007\/3-540-48778-6_12","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"192-210","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Model of Real-Time Program Compilation"],"prefix":"10.1007","author":[{"given":"Karl","family":"Lermer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"Fidge","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"J. A. Bergstra, T. B. Dinesh, J. Field, and J. Heering. A complete transformational toolkit for compilers. Technical Report CS-R9601, Computer Science, Centrum voor Wiskunde en Informatica, January 1996.","DOI":"10.1007\/3-540-61055-3_31"},{"issue":"1","key":"12_CR2","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1093\/comjnl\/39.1.52","volume":"39","author":"E. B\u00f6rger","year":"1996","unstructured":"E. B\u00f6rger and I. Durdanovi\u0107. Correctness of compiling occam to transputer code. The Computer Journal, 39(1):52\u201392, 1996.","journal-title":"The Computer Journal"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"G. J. Chaitin. Register allocation and spilling via graph coloring. ACM SIGPLAN Notices, 17(6), June 1982.","DOI":"10.1145\/872726.806984"},{"key":"12_CR4","unstructured":"C. J. Fidge. Modelling program compilation in the refinement calculus. In D. J. Duke and A. S. Evans, editors, 2nd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer-Verlag, 1997. http:\/\/ewic.springer.co.uk\/workshops\/NFM97\/."},{"key":"12_CR5","unstructured":"C. N. Fischer and R. J. LeBlanc, Jr. Crafting a Compiler. Benjamin\/Cummings, 1988."},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(91)90029-2","volume":"87","author":"P. H. B. Gardiner","year":"1991","unstructured":"P. H. B. Gardiner and C. C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87:143\u2013162, 1991.","journal-title":"Theoretical Computer Science"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"M. Gordon. A formal method for hard real-time programming. In J. M. Morris and R. C. Shaw, editors, 4th Refinement Workshop, pages 378\u2013410. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3756-6_17"},{"key":"12_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Modular Programming Languages","author":"K. J. Gough","year":"1997","unstructured":"K. J. Gough. Multi-target compiler development: Evolution of the Gardens Point compiler project. In H. M\u00f6ssenb\u00f6ck, editor, Modular Programming Languages, volume 1204 of Lecture Notes in Computer Science. Springer-Verlag, 1997."},{"key":"12_CR9","unstructured":"S. Grundon, I. J. Hayes, and C. J. Fidge. Timing constraint analysis. In C. Mc-Donald, editor, Computer Science\u2019 98: Proc. 21st Australasian Computer Science Conference, pages 575\u2013586. Springer-Verlag, 1998."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"R. W. S. Hale. Program compilation. In J. Bowen, editor, Towards Verified Systems, volume 2 of Real-Time Safety Critical Systems, chapter 7, pages 131\u2013146. Elsevier, 1994.","DOI":"10.1016\/B978-0-444-89901-9.50016-1"},{"key":"12_CR11","unstructured":"I. J. Hayes. Separating timing and calculation in real-time refinement. In J. Grundy, M. Schwenke, and T. Vickers, editors, International Refinement Workshop & Formal Methods Pacific\u2019 98, Discrete Mathematics and Theoretical Computer Science, pages 1\u201316. Springer-Verlag, 1998."},{"key":"12_CR12","unstructured":"I. J. Hayes and M. Utting. A sequential real-time refinement calculus. Technical Report 97-33, Software Verification Research Centre, University of Queensland, August 1997. http:\/\/svrc.it.uq.edu.au\/Bibliography\/svrc-tr.html?97-33."},{"key":"12_CR13","unstructured":"He Jifeng. Provably Correct Systems. McGraw-Hill, 1995."},{"key":"12_CR14","unstructured":"C. A. R. Hoare. Refinement algebra proves correctness of compiling specifications. In C. Morgan and J. Woodcock, editors, 3rd Refinement Workshop, pages 33\u201348. Springer-Verlag, 1990."},{"key":"12_CR15","unstructured":"K. Lermer and C. J. Fidge. Compilation as refinement. In L. Groves and S. Reeves, editors, Formal Methods Pacific\u2019 97, pages 142\u2013164. Springer, 1997."},{"key":"12_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1274","DOI":"10.1007\/BFb0002883","volume-title":"Euro-Par\u201997: Parallel Processing","author":"K. Lermer","year":"1997","unstructured":"K. Lermer and C. J. Fidge. A methodology for compilation of high-integrity real-time programs. In C. Lengauer, M. Griebel, and S. Gorlatch, editors, Euro-Par\u201997: Parallel Processing, volume 1300 of Lecture Notes in Computer Science, pages 1274\u201381. Springer-Verlag, 1997. Longer version available as Software Verification Research Centre Technical Report 96-18."},{"key":"12_CR17","unstructured":"K. C. Louden. Compiler Construction: Principles and Practice. PWS Publishing Company, 1997."},{"key":"12_CR18","unstructured":"C. Morgan. Programming from Specifications. Prentice-Hall, second edition, 1994."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to Typed Assembly Language. In Proc. 1998 Symposium on Principles of Programming Languages, San Diego, 1998.","DOI":"10.1145\/268946.268954"},{"key":"12_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"M. M\u00fcller-Olm. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, volume 1283 of Lecture Notes in Computer Science. Springer-Verlag, 1997."},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"T. S. Norvell. Machine code programs are predicates too. In D. Till, editor, Sixth Refinement Workshop, pages 188\u2013204. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3240-0_10"},{"issue":"3","key":"12_CR22","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1145\/256167.256225","volume":"19","author":"N. Ramsey","year":"1997","unstructured":"N. Ramsey and M. F. Fern\u00e1ndez. Specifying representations of machine instructions. ACM Transactions on Programming Languages and Systems, 19(3):492\u2013524, May 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR23","unstructured":"S. Sendall. Semantics of machine instructions. Honours thesis, Department of Computer Science and Electrical Engineering, The University of Queensland, October 1997."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"M. Utting and C. J. Fidge. A real-time refinement calculus that changes only time. In He Jifeng, John Cooke, and Peter Wallis, editors, BCS-FACS Seventh Refinement Workshop, Electronic Workshops in Computing. Springer-Verlag, 1996. http:\/\/ewic.springer.co.uk\/workshops\/7RW\/.","DOI":"10.14236\/ewic\/RW1996.14"},{"key":"12_CR25","unstructured":"D. Watson. High-Level Languages and Their Compilers. Addison-Wesley, 1989."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,21]],"date-time":"2020-04-21T16:34:59Z","timestamp":1587486899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}