{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:43Z","timestamp":1761611203877},"publisher-location":"Berlin, Heidelberg","reference-count":55,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540679592"},{"type":"electronic","value":"9783540445180"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":[[2000]]},"DOI":"10.1007\/3-540-44518-8_11","type":"book-chapter","created":{"date-parts":[[2007,5,26]],"date-time":"2007-05-26T23:44:13Z","timestamp":1180223053000},"page":"177-202","source":"Crossref","is-referenced-by-count":7,"title":["Verifying Compilers and ASMs or ASMs for Uniform Description of Multistep Transformations"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Goos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolf","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,26]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"M. Blum and S. Kannan. Program correctness checking::: and the design of programs that check their work. In Proceedings 21st Symposium on Theory of Computing, 1989.","DOI":"10.1145\/73007.73015"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"M. Blum, M. Luby, and R. Rubinfeld. Self-testing\/correcting with applications to numerical problems. In Proceedings 22nd Symposium on Theory of Computing, 1990.","DOI":"10.1145\/100216.100225"},{"issue":"1","key":"11_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 Kannan. Designing programs that check their work. Journal of the Association for Computing Machinery, 42(1):269\u2013291, January 1995.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR4","unstructured":"Egon Boerger, Igor Durdanovic, and Dean Rosenzweig. Occam: Specification and Compiler Correctness.Part I: The Primary Model. In U. Montanari and E.-R. Olderog, editors, Proc. Procomet\u201994 (IFIP TC2 Working Conference on Programming Concepts, Methods and Calculi). North-Holland, 1994."},{"key":"11_CR5","first-page":"396","volume-title":"IFIP 13th World Computer Congress","author":"E. B\u00f6rger","year":"1994","unstructured":"E. B\u00f6rger, G. Del Castillo, P. Glavan, and D. Rosenzweig. Towards a Mathematical Specification of the APE100 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":"11_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. The Computer Journal, 39(1):52\u201392, 1996.","journal-title":"The Computer Journal"},{"key":"11_CR7","series-title":"Lect Notes Comput Sci","first-page":"151","volume-title":"ZUM\u201997: 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\u201997: The Z Formal Specification Notation, volume 1212 of LNCS, pages 151\u2013187. Springer, 1997."},{"key":"11_CR8","series-title":"Technical Report","volume-title":"The WAM-definition and Compiler Correctness","author":"E. B\u00f6rger","year":"1992","unstructured":"E. B\u00f6rger and D. Rosenzweig. The WAM-definition and Compiler Correctness. Technical Report TR-14\/92, Dip. di informatica, Univ. Pisa, Italy, 1992."},{"key":"11_CR9","unstructured":"E. B\u00f6rger and W. Schulte. A Modular Design for the Java VM architecture. In E. B\u00f6rger, editor, Architecture Design and Validation Methods. Springer, 1998."},{"key":"11_CR10","series-title":"Lect Notes Comput Sci","volume-title":"23rd International Symposium on Mathematical 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 Mathematical Foundations of Computer Science, LNCS. Springer, 1998. To appear."},{"key":"11_CR11","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 Defiunition of the Semantics of Java. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, LNCS. Springer, 1998."},{"key":"11_CR12","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 Lecture Notes in Computer Science, 1992."},{"key":"11_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55984-1_14","volume-title":"Compiler Construction","author":"B. Buth","year":"1992","unstructured":"B. Buth, K.-H. Buth, M. Fr\u00e4nzle, 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":"11_CR14","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."},{"key":"11_CR15","unstructured":"18.-Stephan Diehl. Semantics-Directed Generation of Compilers and Abstract Machines. PhD thesis, University of the Saarland, Germany, 1996."},{"key":"11_CR16","unstructured":"A. Dold, T. Gaul, W. Goerigk, G. Goos, A. Heberle, F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Deffinition of the Language IS. VerifixWorking Paper [Verifix\/UKA\/1], University of Karlsruhe\/Kiel\/Ulm, 1995."},{"key":"11_CR17","unstructured":"A. Dold, T. Gaul, and W. Zimmermann. Mechanized verification of compiler back-ends. In B. Steffen and T. Margaria, editors, Proceedings of the International Workshop on Software Tools for Technology Transfer STTT\u2019 98, pages 13\u201324, Aalborg, Denmark, 1998."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"H. Emmelmann. Code selection by regularly controlled term rewriting. In R. Giegerich and S.L. Graham, editors, Code Generation-Concepts, Tools, Techniques,Workshops in Computing. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3501-2_1"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"H. Emmelmann, F.-W. Schr\u00f6er, and R. Landwehr. Beg-a generator for efficientback ends. In ACM Proceedings of the Sigplan Conference on Programming Language Design and Implementation, June 1989.","DOI":"10.1145\/73141.74838"},{"issue":"6","key":"11_CR20","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1145\/390016.808455","volume":"10","author":"A. Endres","year":"1975","unstructured":"Albert Endres. An analysis of errors and their causes in system programs. SIG-PLAN Notices, 10(6):327\u2013336, 1975.","journal-title":"SIG-PLAN Notices"},{"key":"11_CR21","unstructured":"David A. Espinosa. Semantic Lego. PhD thesis, Columbia University, 1995."},{"key":"11_CR22","unstructured":"T.S. Gaul. An Abstract State Machine Specification of the DEC-Alpha Processor Family. Verifix Working Paper [Verifix\/UKA\/4], Universit\u00e4t Karlsruhe, 1995."},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"W. Goerigk, T.S. Gaul, and W. Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In \u201cProceedings ATOOLS\u201998 Workshop on\u2134ol Support for System Specification, Development, and Verification\u201d, Advances in Computing Science, Malente, 1998. Springer Verl","DOI":"10.1007\/978-3-7091-6355-9_8"},{"key":"11_CR24","unstructured":"Wolfgang Goerigk. Towards Rigorous Compiler Implementation Verification. In Proc. of the 1997 Workshop on Programming Languages and Fundamentals of Programming, Avendorf, Germany, November 1997."},{"key":"11_CR25","first-page":"91","volume":"18","author":"G. Goos","year":"1997","unstructured":"Gerhard Goos. Sather-K-The Language. Software-Concepts and Tools, 18:91\u2013109, 1997.","journal-title":"Software-Concepts and Tools"},{"key":"11_CR26","unstructured":"Y. Gurevich. Evolving Algebras: Lipari Guide. In E. B\u00f6rger, editor, Specification and Validation Methods. Oxford University Press, 1995."},{"key":"11_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-56992-8_17","volume-title":"CSL\u2019 92","author":"Y. Gurevich","year":"1993","unstructured":"Y. Gurevich and J. Huggins. The Semantics of the C Programming Language. In CSL\u2019 92, volume 702 of LNCS, pages 274\u2013308. Springer-Verlag, 1993."},{"key":"11_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Construction of Verified Compiler Front-Ends with Program-Checking","author":"A. Heberle","year":"2000","unstructured":"A. Heberle, T. Gaul, W. Goerigk, G. Goos, and W. Zimmermann. Construction of Verified Compiler Front-Ends with Program-Checking. In Proceedings of PSI\u2019 99: Andrei Ershov Third International Conference on Perspectives Of System Informatics, volume 1755 of Lecture Notes in Computer Science, Novosibirsk, Russia, 1999. Springer Verlag."},{"key":"11_CR29","unstructured":"Andreas Heberle and Dirk Heuzeroth. The formal specification of IS. Technical Report [Verifix\/UKA\/2 revised], IPD, Universit\u00e4t Karlsruhe, January 1998."},{"key":"11_CR30","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"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"J. Huggins and D. Van Campenhout. Specification and Verification of Pipelining in the ARM2 RISC Microprocessor. ACM Transactions on Design Automation of Electronic Systems, 3(4):563\u2013580, October 1998.","DOI":"10.1145\/296333.296345"},{"issue":"5","key":"11_CR32","first-page":"416","volume":"3","author":"P. W. Kutter","year":"1997","unstructured":"P. W. Kutter and A. Pierantonio. Montages specifications of realistic programming languages. Journal of Universal Computer Science, 3(5):416\u2013442, 1997.","journal-title":"Journal of Universal Computer Science"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"John McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Schwartz [51], pages 33\u201341.","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"11_CR34","unstructured":"Sun Microsystems. Sun official java compiler bug database. http:\/\/java.sun.com\/products\/jdk\/1.2\/bugs.html , mar 2000."},{"key":"11_CR35","unstructured":"J S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996."},{"key":"11_CR36","unstructured":"C. Robert Morgan. Building an Optimizing Compiler. Digital Press, Februar 1998. ISBN 155558179X."},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"P. D. Mosses. Abstract semantic algebras. In D. Bj\u00f8rner, editor, Formal description of programming concepts II, pages 63\u201388. IFIP IC-2 Working Conference, North Holland, 1982.","DOI":"10.7146\/dpb.v11i145.6543"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"P. D. Mosses. Action Semantics. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511569869"},{"key":"11_CR39","unstructured":"Markus M\u00fcller-Olm. An Exercise in Compiler Verification. Internal report, CS Department, University of Kiel, 1995."},{"key":"11_CR40","volume-title":"Modular Compiler Verification","author":"M. M\u00fcller-Olm","year":"1996","unstructured":"Markus M\u00fcller-Olm. Modular Compiler Verification. PhD thesis, Techn. Fakult\u00e4t der Christian-Albrechts-Universit\u00e4t, Kiel, June 1996."},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Jens Palsberg. Provably Correct Compiler Generation. PhD thesis, Department of Computer Science, University of Aarhus, 1992. xii+224 pages.","DOI":"10.7146\/dpb.v21i422.6736"},{"key":"11_CR42","unstructured":"L. Paulson. A compiler generator for semantic grammars. PhD thesis, Stanford University, 1981."},{"key":"11_CR43","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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 Systems, volume 1384 of Lecture Notes in Computer Science, pages 151\u2013166. Springer-Verlag, 1998."},{"issue":"2","key":"11_CR44","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":"11_CR45","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 Lecture Notes in Computer Science, number 124 in LNCS. Springer-Verlag, 1981."},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"Robert M. Poston. Preventing software requirements specification errors with ieee 830. IEEE Software, 2(1):83\u201386, January 1985.","DOI":"10.1109\/MS.1985.230053"},{"key":"11_CR47","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":"11_CR48","doi-asserted-by":"crossref","unstructured":"J. T. Schwartz, editor. Mathematical Aspects of Computer Science, Proc. Symp. in Appl. Math., RI, 1967. Am. Math. Soc.","DOI":"10.1090\/psapm\/019"},{"key":"11_CR49","unstructured":"Reinier Sterkenburg. Borland pascal compiler bug list. http:\/\/www.dataweb.nl\/r.p.sterkenburg\/bugsall.htm , feb 2000."},{"key":"11_CR50","doi-asserted-by":"crossref","unstructured":"M. Tofte. Compiler Generators. Springer-Verlag, 1990.","DOI":"10.1007\/978-3-642-61504-7"},{"key":"11_CR51","doi-asserted-by":"crossref","unstructured":"William M. Waite and Gerhard Goos. Compiler Construction. Springer-Verlag, 1984.","DOI":"10.1007\/978-1-4612-5192-7"},{"key":"11_CR52","unstructured":"C. Wallace. The Semantics of the C++ogramming Language. In E. B\u00f6rger, editor, Specification and Validation Methods. Oxford University Press"},{"key":"11_CR53","doi-asserted-by":"crossref","unstructured":"M. Wand. A semantic prototyping system. SIGPLAN Notices, 19(6):213\u2013221, June 1984. SIGPLAN 84 Symp. On Compiler Construction.","DOI":"10.1145\/502949.502895"},{"key":"11_CR54","doi-asserted-by":"crossref","unstructured":"Hal Wasserman and Manuel Blum. Software reliability via run-time result-checking. Journal of the ACM, 44(6):826\u2013849, November 1997.","DOI":"10.1145\/268999.269003"},{"key":"11_CR55","unstructured":"W. Zimmermann and T. Gaul. An Abstract State Machine for Java Byte Code. Verifix Working Paper [Verifix\/UKA\/12], University of Karlsruhe, 1997."}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines - Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44518-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:02:15Z","timestamp":1556449335000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44518-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540679592","9783540445180"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/3-540-44518-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}