{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:18:07Z","timestamp":1725488287908},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664628"},{"type":"electronic","value":"9783540482574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48257-1_7","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T16:25:09Z","timestamp":1184948709000},"page":"122-136","source":"Crossref","is-referenced-by-count":3,"title":["Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Goerigk","sequence":"first","affiliation":[]},{"given":"Ulrich","family":"Hoffmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"7_CR1","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/200836.200880","volume":"42","author":"M. Blum","year":"1995","unstructured":"Manuel Blum and Sampath Kannan. Designing programs that check their work. Journal of the ACM, 42(1):269\u2013291, January 1995.","journal-title":"Journal of the ACM"},{"key":"7_CR2","unstructured":"Bettina Buth and Markus M\u00fcller-Olm. Provably Correct Compiler Implementation. In Tutorial Material-Formal Methods Europe\u2019 93, pages 451\u2013465, Denmark, April 1993. IFAD Odense Teknikum."},{"issue":"2","key":"7_CR3","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/5397.30847","volume":"8","author":"L.M. Chirica","year":"1986","unstructured":"L.M. Chirica and D.F. Martin. Toward Compiler Implementation Correctness Proofs. ACM Transactions on Programming Languages and Systems, 8(2):185\u2013214, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR4","unstructured":"Paul Curzon. The Verified Compilation of Vista Programs. Internal Report, Computer Laboratory, University of Cambridge, January 1994."},{"key":"7_CR5","unstructured":"Wolfgang Goerigk. An Exercise in Program Verification: The ACL2 Correctness Proof of a Simple Theorem Prover Executable. Veri\/iz-Arbeitsbericht Verifix\/CAU\/2.4, CAU Kiel, 1996."},{"key":"7_CR6","unstructured":"Wolfgang Goerigk. A Denotational Semantics for ComLisp and SIL. Verifix-Arbeitsbericht Verifix\/CAU\/2.8, CAU Kiel, December 1997."},{"key":"7_CR7","unstructured":"Wolfgang Goerigk, Axel Dold, Thilo Gaul, Gerhard Goos, Andreas Heberle, Friedrich W. von Henke, Ulrich Hoffmann, Hans Langmaack, Holger Pfeifer, Harald Ruess, and Wolf Zimmermann. Compiler Correctness and Implementation Verification: The Verifix Approach. In P. Fritzson, editor, Proceedings of the Poster Session of CC\u2019 96-International Conference on Compiler Construction, IDA Technical Report LiTH-IDA-R-96-12, Link\u00f8ping, Sweden, 1996."},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Wolfgang Goerigk, Thilo Gaul, and Wolf Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Proceedings ATOOLS\u201998 Workshop on \u201cTool Support for System Specification, Development, and Verification\u201d, Advances in Computer Science, Malente, 1998. Springer Verlag. To Appear.","DOI":"10.1007\/978-3-7091-6355-9_8"},{"key":"7_CR9","unstructured":"Wolfgang Goerigk and Ulrich Hoffmann. The Compiler Implementation Language ComLisp. Verifix-Arbeitsbericht Verifix\/CAU\/1.7, CAU Kiel, June 1996."},{"key":"7_CR10","series-title":"Technical Report","volume-title":"The Compiling Specification from ComLisp to Executable Machine Code","author":"W. Goerigk","year":"1998","unstructured":"Wolfgang Goerigk and Ulrich Hoffmann. The Compiling Specification from ComLisp to Executable Machine Code. Technical Report Nr. 9713, Institut f\u00fcr Informatik, CAU, Kiel, December 1998. In Preparation."},{"key":"7_CR11","unstructured":"Wolfgang Goerigk and Markus M\u00fcller-Olm. Erhaltung partieller Korrektheit bei beschr\u00e4nkten Maschinenressourcen.-Eine Beweisskizze-. Verifix-Arbeitsbericht Verifix\/CAU\/2.5, CAU Kiel, 1996."},{"issue":"6","key":"7_CR12","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1145\/390016.808473","volume":"10","author":"J.B. Goodenough","year":"1975","unstructured":"J.B. Goodenough and S.L. Gerhart. Toward a Theory of Test Data Selection. SIGPLAN Notices, 10(6):493\u2013510, June 1975.","journal-title":"SIGPLAN Notices"},{"key":"7_CR13","unstructured":"Ulrich Hoffmann, \u00dcber die korrekte Implementierung von Compilern. In Work shop \u201cAlternative Konzepte f\u00fcr Sprachen und Rechner\u201d, Bad Honnef, 1996. Auch erschienen als Verifix-Arbeitsbericht Verifix\/CAU\/3.1."},{"key":"7_CR14","series-title":"Arbeitsbericht des Institutes f\u00fcr Wirtschaftsinformatik","volume-title":"Arbeitstagung Programmiersprachen","author":"U. Hoffmann","year":"1997","unstructured":"Ulrich Hoffmann. Korrekte Implementierung von \u00dcbersetzungsspezifikationen in hoher Programmiersprache. In Herbert Kuchen, editor, Arbeitstagung Programmiersprachen, volume 58 of Arbeitsbericht des Institutes f\u00fcr Wirtschaftsinformatik. Westf\u00e4lische Wilhelms-Universit\u00e4t M\u00fcnster, 1997."},{"key":"7_CR15","unstructured":"Inmos Limited. Transputer instruction set: A compiler writer\u2019s guide, 1988."},{"key":"7_CR16","volume-title":"Systematic Software Development Using VDM","author":"C. B. Jones","year":"1990","unstructured":"C. B. Jones. Systematic Software Development Using VDM, 2nd ed. Prentice Hall, New York, London, 1990.","edition":"2nd ed."},{"key":"7_CR17","unstructured":"M. Kaufmann and J S. Moore. Design Goals of ACL2. Technical Report 101, Computational Logic, Inc., August 1994."},{"key":"7_CR18","unstructured":"H. Langmaack. Ein Beitrag zu Goodenoughs und Gerharts Theorie des Softwaretestens und-verifizierens: Beziehungen zwischen starkem \u00dcbersetzertest und \u00dcbersetzerimplementierungsverifikation. Foundations of Computer Science: The ory, Cognition, Applications, Springer Verlag., 1996. In Preparation."},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Hans Langmaack. Softwareengineering zur Zertifizierung von Systemen: Spezifikations-, Implementierungs-, \u00dcbersetzerkorrektheit. Informationstechnik und Technische Informatik it-ti, 1997.","DOI":"10.1524\/itit.1997.39.3.41"},{"key":"7_CR20","volume-title":"Korrektheit der Daten-und Operationsverfeinerung f\u00fcr eine applikative Sprache mit automatischer Speicherbereinigung","author":"D. Michelsen","year":"1998","unstructured":"Dagobert Michelsen. Korrektheit der Daten-und Operationsverfeinerung f\u00fcr eine applikative Sprache mit automatischer Speicherbereinigung. Master\u2019s thesis, Institut f\u00fcr Informatik, CAU, Kiel, 1998."},{"key":"7_CR21","series-title":"Technical Report","volume-title":"Piton: A verified assembly level language","author":"J. S. Moore","year":"1988","unstructured":"J S. Moore. Piton: A verified assembly level language. Technical Report 22, Comp. Logic Inc, Austin, Texas, 1988."},{"key":"7_CR22","unstructured":"Markus M\u00fcller-Olm. Three Views on Preservation of Partial Correctness. Verifix-Arbeitsbericht Verifix\/CAU\/5.1, CAU Kiel, October 1996."},{"key":"7_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"Markus M\u00fcller-Olm. Modular Compiler Verification, volume 1283 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Heidelberg, New York, 1997."},{"key":"7_CR24","unstructured":"Dino P. Oliva and Mitchell Wand. A Verified Compiler for Pure PreScheme. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, Northeastern University, February 1992."},{"key":"7_CR25","unstructured":"Holger Pfeifer, Axel Dold, F.W. von Henke, and Harald Rue\u00df. Mechanized Semantics of Simple Imperative Programming Constructs. Ulmer Informatik-Berichte 96\u201311, Universit\u00e4t Ulm, December 1996."},{"key":"7_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10886-6","volume-title":"Lecture Notes in Computer Science","author":"W. Polak","year":"1981","unstructured":"W. Polak. Compiler specification and verification. In J. Hartmanis G. Goos, editor, Lecture Notes in Computer Science, number 124 in LNCS. Springer-Verlag, 1981."},{"issue":"8","key":"7_CR27","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1145\/358198.358210","volume":"27","author":"K. Thompson","year":"1984","unstructured":"Ken Thompson. Reflections on Trusting Trust. Communications of the ACM, 27(8):761\u2013763, 1984. Also in ACM Turing Award Lectures: The First Twenty Years 1965\u20131985, ACM Press, 1987, and in Computers Under Attack: Intruders, Worms, and Viruses Copyright, ACM Press 1990.","journal-title":"Communications of the ACM"},{"issue":"6","key":"7_CR28","doi-asserted-by":"publisher","first-page":"826","DOI":"10.1145\/268999.269003","volume":"44","author":"H. Wasserman","year":"1997","unstructured":"Hal Wasserman and Manuel Blum. Software reliability via run-time result-checking. Journal of the ACM, 44(6):826\u2013849, November 1997.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Applied Formal Methods \u2014 FM-Trends 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48257-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T07:08:18Z","timestamp":1556694498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48257-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664628","9783540482574"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-48257-1_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}