{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:09:21Z","timestamp":1781651361969,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540666240","type":"print"},{"value":"9783540480921","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48092-7_10","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T13:01:46Z","timestamp":1186750906000},"page":"201-230","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":34,"title":["Verification of Compilers"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Goos","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolf","family":"Znnmerrnaun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2000,3,24]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"M. Blum and S. Karman. Program correctness checking... and the design of programs that check their work. In Proceedings 21st Stnnpoeuuti on Theory of Computing, 1989.","DOI":"10.1145\/73007.73015"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"M. Blum, M. Luby, and R. Rubinfeld. Self-testingycorrecting with applications to numerical problems. In Proceedings 22nd Symposium on Theory of Computing, 1990.","DOI":"10.1145\/100216.100225"},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/200836.200880","volume":"42","author":"M. Blum","year":"1995","unstructured":"Manuel Blum and Sampath Karman. Designing programs that check their work. Journal of the ACM; 42(1):269\u2013291, January 1995.","journal-title":"Journal of the ACM"},{"key":"10_CR4","first-page":"396","volume-title":"IFIP 13th World Computer Congress volume I: Technology\/Foundations","author":"E. Borger","year":"1994","unstructured":"E. Borger, G. Del Castillo, P. Glavan, and D. Rosenzweig. Towards a Mathematical Specification of the APElOO Architecture: the APESE Model. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress volume I: Technology\/Foundations, pages 396\u2013401, Elsevier, Amsterdam, the Netherlands, 1994."},{"issue":"1","key":"10_CR5","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. Durdanovic. Correctness of compiling occam to transputer. The Computer Journal, 39(1):52\u201392, 1996.","journal-title":"The Computer Journal"},{"key":"10_CR6","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. Durdanovic. Correctness of Compiling Occam to Transputer code. The Computer Journal, 39:52\u201393, 1996.","journal-title":"The Computer Journal"},{"key":"10_CR7","unstructured":"E. B\u00f6rger, I. Durdanovic, and D. Rosenzweig. Occam: Specification and Compiler Correctness.Part I: The Primary Model. In U. Montanari and E.-R. Olderog, editors, Proc. Procomet'94 (IFIP TC2 VVorking Conference on Proqmmminq Concepts, Methods and Calculi). North-Holland, 1994."},{"key":"10_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0027289","volume-title":"ZUM'91: The Z Formal Specification Notation","author":"E. B\u00f6rger","year":"1997","unstructured":"E. B\u00f6rger and S. Mazzanti. A Practical Method for Rigorously Controllable Hardware Design. In J.P. Bowen, M.B. Hinchey, and D. Till, editors, ZUM'91: The Z Formal Specification Notation, volume 1212 of LNCS, pages 151\u2013187. Springer, 1997."},{"key":"10_CR9","unstructured":"E. B\u00f6rger and D. Rosenzweig. The WAM-definition and Compiler Correctmese. North-Holland Series in Computer Science and Artificial Intelligence. Beierle, L.C. and Pluemer, L., 1994."},{"key":"10_CR10","unstructured":"E. B\u00f6rger and W. Schulte. A Modular Design for the Java VM architecture. In E. Borger, editor, Architecture Design and Validation Methods. Springer, 1998."},{"key":"10_CR11","series-title":"Lect Notes Comput Sci","volume-title":"23rd international Symposium on Motbcouuicol Foundations of Computer Science","author":"E. B\u00f6rger","year":"1998","unstructured":"E. B\u00f6rger and W. Schulte. Defining the Java Virtual Machine as Platform for Provably Correct Java Compilation. In 23rd international Symposium on Motbcouuicol Foundations of Computer Science, LNCS. Springer, 1998. To appear."},{"key":"10_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Formal Syntax and Semantics of Java","author":"E. B\u00f6rger","year":"1998","unstructured":"E. B\u00f6rger and W. Schulte. Programmer Friendly Modular Definition of the Semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS. Springer, 1998."},{"key":"10_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Compiler Compilers 92","author":"D. F. Brown","year":"1992","unstructured":"D. F. Brown, H. Moura, and D. A. Watt. Actress: an action semantics directed compiler generator. In Compiler Compilers 92, volume 641 of LNCS, 1992."},{"key":"10_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-55215-4","volume-title":"Compiler Construction","author":"B. Buth","year":"1992","unstructured":"B. Buth, K.-H. Buth, M. Franzle, B. v. Karger, Y. Lakhneche, H. Langmaack, and M. M\u00fcller-Olm. Provably correct compiler development and implementation. In U. Kastens and P. Pfahler, editors, Compiler Construction. volume 641 of LNCS. Springer-Verlag, 1992."},{"key":"10_CR15","unstructured":"B. Buth and M. M\u00fcller-Olm. Provably Correct Compiler Implementation. In Tutorial Material-Formal Methods Europe '93, pages 451\u2013465, Denmark, April 1993. IFAD Odense Teknikum."},{"key":"10_CR16","series-title":"PhD thesis","volume-title":"Senuuitics-Dlrected Generation of Compilers and Abstract Machines","author":"S. Diehl","year":"1996","unstructured":"Stephan Diehl. Senuuitics-Dlrected Generation of Compilers and Abstract Machines. PhD thesis, Univerait\u00e4t des Saarlandes, Germany, 1996."},{"key":"10_CR17","unstructured":"A. Dold, T. Gaul, W. Coerigk, G. Coos, A. Heberle F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeiffer, H. Ruess, and W. Zimmermann. The semantics of a while language ISo. Working paper, The VERIFIX Group, July '95, 1995."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"H. Emmelmann, F.-W. Schr\u00f6er, and R. Landwehr. Beg a generator for efficient back ends. In ACM Proceedings of the Sigplan Conference on Programming Language Design and Implementation, June 1989.","DOI":"10.1145\/73141.74838"},{"key":"10_CR19","unstructured":"David A. Espinosa. Semantic Lego. PhD thesis, Columbia University, 1995."},{"key":"10_CR20","unstructured":"T. Gaul, A. Heberle, W. Zimmermann, and W. Goerigk. Construction of Verified Software Systems with Program-Checking: An Application To Compiler Back-Ends. In Proceedings of the Federated Loqics Conference (FloC99) VVorkshop on Runtime Result verification,Trento, Italy, 1999. Electronic Proceedings, URL:http:\/\/afrodite.itc.it:1024\/~leaf\/rtrv\/proc\/proc.html."},{"key":"10_CR21","unstructured":"T.S. Gaul. An Abstract State Machine Specification of the DEC-Alpha Processor Family. Verifix Working Paper [Verifix\/UKA\/41], University of Karlsruhe, 1995."},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Wolfgang Coerigk, Thilo Gaul, and Wolf Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Proceedings ATOOLS'98 VVorkshop on \u201cTool Support for System Specification, Development, and Verificationt\u201d, Advances in Computing Science, Malente, 1998. Springer Verlag. Accepted for Publication.","DOI":"10.1007\/978-3-7091-6355-9_8"},{"key":"10_CR23","first-page":"91","volume":"18","author":"G. Goos","year":"1997","unstructured":"Gerhard Goos. Sather\u2013k \u2014the language. Software \u2014Concepts and Tools, 18: 91\u2013109, 1997.","journal-title":"Software \u2014Concepts and Tools"},{"key":"10_CR24","unstructured":"Y. Gurevich. Evolving Algebras: Lipari Guide. In E. Borger, editor, Specification and Validation Methode. Oxford University Press, 1995."},{"key":"10_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-56992-8_17","volume-title":"CSL '92","author":"Y. Gurevich","year":"1993","unstructured":"Y. Gurevich and J. Huggins. The Semantics of the C Programming Language. In CSL '92, volume 702 of LNCS, pages 274\u2013308. Springer-Verlag, 1993"},{"key":"10_CR26","first-page":"370","volume-title":"Construction of Verified Compiler Front-Ends with Program-Checking","author":"A. Heberle","year":"1999","unstructured":"A. Heberle, T. Gaul, W. Coerigk, G. Coos, and W. Zimmermann. Construction of Verified Compiler Front-Ends with Program-Checking. In Proceeduiqe of PSI '99: Andrei Erehou Third International Conference on Perspectiues Of System Infotmatics, pages 370\u2013377, Novosibirsk, Russia, 1999."},{"key":"10_CR27","unstructured":"Andreas Heberle and Dirk Heuzeroth. The formal specification of IS. Technical Report [Verifix\/UKA\/2 revised], IPD, Univerait\u00e4t Karlsruhe, January 1998."},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"C.A.R. Hoare","year":"1993","unstructured":"C.A.R. Hoare, He Jifeng, and A. Sampaio. Normal Form Approach to Compiler Design. Acta informatica, 30:701\u2013739, 1993","journal-title":"Acta informatica"},{"issue":"4","key":"10_CR29","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1145\/296333.296345","volume":"3","author":"J. Huggins","year":"1998","unstructured":"J. Huggins and D. Van Campenhout. Specification and Verification of Pipelining in the ARM2 RISC Microprocessor. ACM Transactions on Design Automation of Electronic System, 3(4):563\u2013580, October 1998.","journal-title":"ACM Transactions on Design Automation of Electronic System"},{"key":"10_CR30","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0304-3975(97)00267-3","volume":"199","author":"T.M.V. Janssen","year":"1998","unstructured":"T.M.V. Janssen. Algebraic translations, correctness and algebraic compiler construction. Theoretical Computer Science, 199:25\u201356, 1998.","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"10_CR31","first-page":"416","volume":"3","author":"P. W. Kutter","year":"1997","unstructured":"P. W. Kutter and A. Pierantonio. Montages specifications of realisitic programming languages. Journal of Uniuersol Computer Science, 3(5):416\u2013442, 1997.","journal-title":"Journal of Uniuersol Computer Science"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"John McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Schwartz, pages 33\u201341.","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"10_CR33","unstructured":"J S. Moore. Piton, MEchanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996."},{"key":"10_CR34","unstructured":"P. D. Mosses. Abstract semantic algebras. In D. Bj\u2205rner, editor, Formal description of programming concepts II, pages 63\u201388. IFIP IC-2 Working Conference, North Holland, 1982."},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"P. D. Mosses. Action Semantics. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511569869"},{"key":"10_CR36","series-title":"Internal report","volume-title":"An Exercise in Compiler Verification","author":"M. M\u00fcller-Olm","year":"1995","unstructured":"Markus M\u00fcller-Olm.An Exercise in Compiler Verification. Internal report, CS Department, Univerait\u00e4t Kiel, 1995."},{"key":"10_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0017806","volume-title":"Modular Compiler Verification","author":"M. M\u00fcller-Olm","year":"1996","unstructured":"Markus M\u00fcller-Olm. Modular Compiler Verification, volume 1283 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"J. Palsberg. An automatically generated and provably correct compiler for a subset of ada. In IEEE International Conference on Computer Language, 1992.","DOI":"10.7146\/dpb.v21i383.6615"},{"key":"10_CR39","series-title":"PhD thesis","first-page":"xii+224","volume-title":"Provably Correct Compiler Generation","author":"J. Palsberg","year":"1992","unstructured":"Jens Palsberg. Provably Correct Compiler Generation. PhD thesis, Department of Computer Science, University of Aarhus, 1992. xii+224 pages."},{"key":"10_CR40","unstructured":"L. Paulson. A compiler generator for semantic grammars. PhD thesis, Stanford University, 1981."},{"key":"10_CR41","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"In Tools and Algorithms for the Construction and Analysis of System","author":"A. Pnueli","year":"1998","unstructured":"A. Pnueli, M. Siegel, and E. Singermann. Translation validation. In Tools and Algorithms for the Construction and Analysis of System, volume 1384 of Lecture Notes in Computer Science pages 151\u2013166. Springer-Verlag, 1998."},{"issue":"2","key":"10_CR42","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/s100090050027","volume":"2","author":"A. Pnueli","year":"1998","unstructured":"Amir Pnueli, O. Shtrichman, and M. Siegel. The code validation tool (cvt). Int. J. on Software Tools for Technology Transfer, 2(2):192\u2013201, 1998.","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"key":"10_CR43","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10886-6","volume-title":"Compiler Specification and Verification","author":"W. Polak","year":"1981","unstructured":"W. Polak. Compiler Specification and Verification, volume 124 of LNCS. Springer-Verlag, Berlin, Heidelberg, New York, 1981."},{"key":"10_CR44","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0304-3975(97)00270-3","volume":"199","author":"T. Rus","year":"1998","unstructured":"T. Rus. Algebraic processing of programming languages. Theoretical Computer Science, 199:105\u2013143, 1998.","journal-title":"Theoretical Computer Science"},{"key":"10_CR45","unstructured":"J. T. Schwartz, editor Mathematical Aspects of Computer Science, Proc. Symp. in Appl.:Math., RI, 1967. Am.:Math. Soc."},{"issue":"8","key":"10_CR46","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.","journal-title":"Communications of the ACM"},{"key":"10_CR47","doi-asserted-by":"crossref","unstructured":"M. Tofte. Compiler Generators. Springer-Verlag, 1990.","DOI":"10.1007\/978-3-642-61504-7"},{"key":"10_CR48","unstructured":"C. Wallace. The Semantics of the C++Programming Language. In E. B\u00f6rger, editor, Specification and Validation Methods. Oxford University Press, 1995."},{"issue":"6","key":"10_CR49","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/502949.502895","volume":"19","author":"M. Wand","year":"1984","unstructured":"M. Wand.A semantic prototyping system. SIGPLAN Notices, 19(6):213\u2013221, June 1984. SIGPLAN 84 Symp. On Compiler Construction.","journal-title":"SIGPLAN Notices"},{"issue":"6","key":"10_CR50","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"},{"key":"10_CR51","unstructured":"W. Zimmermann and T. Gaul. An Abstract State Machine for Java, Byte Code. Verifix Working Paper [Verifix\/UKA\/121, University of Karlsruhe, 1997."},{"issue":"5","key":"10_CR52","first-page":"504","volume":"3","author":"W. Zimmermann","year":"1997","unstructured":"W. Zimmermann and T. Gaul. On the Construction of Correct Compiler Back-Ends: An ASM Approach. Journal of Universal Computer Science, 3(5):504\u2013567, 1997.","journal-title":"Journal of Universal Computer Science"}],"container-title":["Lecture Notes in Computer Science","Correct System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48092-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:52:50Z","timestamp":1778248370000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-48092-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540666240","9783540480921"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/3-540-48092-7_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"24 March 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}