{"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":1781651361384,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540671022","type":"print"},{"value":"9783540465621","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46562-6_43","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T00:12:56Z","timestamp":1194999176000},"page":"481-492","source":"Crossref","is-referenced-by-count":5,"title":["Construction of Verified Compiler Front-Ends with Program-Checking"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Heberle","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thilo","family":"Gaul","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolfgang","family":"Goerigk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gerhard","family":"Goos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolf","family":"Zimmermann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2000,1,28]]},"reference":[{"key":"43_CR1","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"},{"issue":"1","key":"43_CR2","doi-asserted-by":"crossref","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":"43_CR3","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":"43_CR4","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. Definition of the Language IS. Verifix Working Paper [Verifix\/UKA\/1], University of Karlsruhe\/Kiel\/Ulm, 1995."},{"key":"43_CR5","unstructured":"A.[Dold, T.[Gaul, V.[Vialard, and W.[Zimmermann. H. Schmitt, editors, Proceedings of the 5th International Workshop on Abstract State Machines, pages 50\u201367, 199"},{"key":"43_CR6","volume-title":"PhD thesis","author":"S. Diehl","year":"1996","unstructured":"Stephan Diehl. Semantics-Directed Generation of Compilers and Abstract Machines. PhD thesis, University of the Saarland, Germany, 1996."},{"key":"43_CR7","unstructured":"W. Goerigk, A. Dold, T. Gaul, G. Goos, A. Heberle, F. von Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Compiler Correctness and Implementation Verification: The Verifix Approach. In P. Fritzson, editor, Proceedings of the Poster Session of CC\u201996-International Conference on Compil er Construction, pages 65\u201373. ida, 1996. TR-Nr.: R-96-12."},{"key":"43_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Compiler Compilers, Third International Workshop, CC\u201990; Schwerin, FRG; Proceedings","author":"J. Grosch","year":"1990","unstructured":"J. Grosch and H. Emmelmann. A tool box for compiler construction. In Compiler Compilers, Third International Workshop, CC\u201990; Schwerin, FRG; Proceedings, volume 477 of LNCS. Springer-Verlag, 1990."},{"issue":"6","key":"43_CR9","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":"43_CR10","doi-asserted-by":"crossref","unstructured":"W. Goerigk, T.S. Gaul, and W. Zimmermann. Correct Programs without Proof? On Checker-Based Program Verification. In Proceedings ATOOLS\u201998 Workshop on \u201cTool Support for System Speciciation, Development, and Verification\u201d, Advances in Computing Science, Malente, 1998. Springer Verlag.","DOI":"10.1007\/978-3-7091-6355-9_8"},{"key":"43_CR11","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":"43_CR12","unstructured":"A. Heberle and T. Gaul. Syntax einer Sprache zur textuellen Repr\u00e4sentation von Graphen Interner Bericht, 1998."},{"key":"43_CR13","unstructured":"Andreas Heberle and Dirk Heuzeroth. The formal specification of IS. Technical Report [Verifix\/UKA\/2 revised], IPD, Universit\u00e4t Karlsruhe, January 1998."},{"key":"43_CR14","doi-asserted-by":"crossref","unstructured":"G. C. Necula and P. Lee. The design and implementation of a certifying compiler. In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 333\u2013344, 1998.","DOI":"10.1145\/277650.277752"},{"key":"43_CR15","unstructured":"M. Pettersson. Compiling Natural Semantics. PhD thesis, Linkoeping University, 1995."},{"issue":"6","key":"43_CR16","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","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46562-6_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T11:26:46Z","timestamp":1556969206000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46562-6_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671022","9783540465621"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-46562-6_43","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}