{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:09:58Z","timestamp":1761610198655,"version":"build-2065373602"},"reference-count":40,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4137,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,4]]},"DOI":"10.1016\/s1571-0661(04)80394-3","type":"journal-article","created":{"date-parts":[[2004,9,28]],"date-time":"2004-09-28T15:29:25Z","timestamp":1096385365000},"page":"19-36","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verified Code Generation for Embedded Systems"],"prefix":"10.1016","volume":"65","author":[{"given":"Sabine","family":"Glesner","sequence":"first","affiliation":[]},{"given":"Rubino","family":"Gei\u00df","sequence":"additional","affiliation":[]},{"given":"Boris","family":"Boesler","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB1","unstructured":"U. A\u00dfmann, D. Genius, P. Fritzson, H. Sips, R. Kurver, R. Wilhelm, H. Schepers, and T. Rindborg. Java and cosy technology for embedded systems: The joses project. In Proc. of the European Multimedia, Microprocessor Systems, Technologies for Business Processing and Electronic Commerce Conference (EMMSEC'99), Stockholm, Sweden, 1999."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB2","doi-asserted-by":"crossref","unstructured":"M. Blum and S. Kannan. Program correctness checking \u2026 and the design of programs that check their work. In Proceedings 21st Symposium on Theory of Computing, 1989.","DOI":"10.1145\/73007.73015"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB3","doi-asserted-by":"crossref","unstructured":"M. Blum and S. Kannan. Designing programs that check their work. Journal of the ACM, 42(1):269\u2013291, 1995. Preliinary version: Proc. 21st ACM Symp. Theory of Computing (1989), pp. 86\u201397.","DOI":"10.1145\/200836.200880"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Steven Bashford and Rainer Leupers. Constraint Driven Code Selection for Fixed-Point DSPs. In 36th Design Automation Conference, New Orleans (USA), June 1999.","DOI":"10.1145\/309847.310076"},{"issue":"2\/3","key":"10.1016\/S1571-0661(04)80394-3_NEWBIB5","article-title":"Phase-Coupled Mapping of Data Flow Graphs to Irregular Data Paths","volume":"4","author":"Bashford","year":"1999","journal-title":"Design Automation for Embedded Systems"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB6","unstructured":"Shuvra S. Bhattacharyya, Rainer Leupers, and Peter Marwedel. Software Synthesis and Code Generation for Signal Processing Systems. Technical Report Technical report UMIACS-TR-99-57, Institute for Advanced Computer Studies, University of Maryland, College Park 20742, USA, September 1999."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB7","doi-asserted-by":"crossref","unstructured":"M. Blum, M. Luby, and R. Rubinfeld. Self-Testing\/Correcting with Applications to Numerical Problems. Journal of Computer and System Sciences, 47(3):549\u2013595, 1993. Preliminary version: Proc. 22nd ACM Symp. Theory of Computing (1990), pp. 73\u201383.","DOI":"10.1016\/0022-0000(93)90044-W"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB8","unstructured":"Boris Boesler. Codeerzeugung aus Abh\u00e4ngigkeitsgraphen. Diplomarbeit, Universit\u00e4t Karlsruhe, June 1998."},{"issue":"3","key":"10.1016\/S1571-0661(04)80394-3_NEWBIB9","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1145\/203095.203099","article-title":"Efficiently Computing \u03a6-Nodes On-The-Fly","volume":"17","author":"Cytron","year":"1995","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB10","doi-asserted-by":"crossref","unstructured":"R. Cytron, J. Ferrante, and B. K. Rosen. An efficient method of computing static single assignment form. In Conference Record of the 16th Annual ACM Symposium on Principles of Programming Languages (POPL'89), pages 25\u201335. ACM-SIGACT, ACM Press, 1989.","DOI":"10.1145\/75277.75280"},{"issue":"4","key":"10.1016\/S1571-0661(04)80394-3_NEWBIB11","first-page":"451","article-title":"Efficiently computing static single assignment form and the control dependence graph","volume":"13","author":"Cytron","year":"1991","journal-title":"Sigplan Notices"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB12","unstructured":"Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A Certifying Compiler for Java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00), 2000."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB13","unstructured":"Axel Dold, Thilo Gaul, and Wolf Zimmermann. Mechanized verification of compiler backends. In Proceedings of the International Workshop on Software Tools for Technology Transfer (STTT'98), 1998."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB14","series-title":"Code Generation - Concepts, Tools, Techniques, Workshops in Computing","article-title":"Code selection by regularly controlled term rewriting","author":"Emmelmann","year":"1992"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB15","unstructured":"Helmut Emmelmann. Codeselektion mit regul\u00e4r gesteuerter Termersetzung. PhD thesis, Universit\u00e4t Karlsruhe, Fakult\u00e4t f\u00fcr Informatik, May 1994."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB16","doi-asserted-by":"crossref","unstructured":"H. Emmelmann, F.-W. Schrer, and R. Landwehr. BEG - A Generator for Efficient Back Ends. In ACM Proceedings of the Sigplan Conference on Programming Languages Design and Implementation, June 1989.","DOI":"10.1145\/73141.74838"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB17","unstructured":"Thilo Gaul, Andreas Heberle, Wolf Zimmermann, and Wolfgang Goerigk. Construction of verified software systems with program-checking: An application to compiler back-ends. In Proceedings of the Workshop on Runtime Result Verification (RTRV'99), 1999."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB18","unstructured":"Thilo Gaul and Antonio Kung. AJACS: Applying Java to Automotive Control Systems. In Conference Proceedings of Embedded Intelligence Conference, Nrnberg. Conference Proceedings Embedded Intelligence 2001, Feb 2001."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB19","first-page":"201","article-title":"Verification of Compilers","volume":"vol. 1710","author":"Goos","year":"1999"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB20","doi-asserted-by":"crossref","unstructured":"Gerhard Goos and Wolf Zimmermann. Verifying Compilers and ASMs or ASMs for uniform description of multistep transformations. In ASM-2000. Springer-Verlag, Lecture Notes in Computer Science, 2000.","DOI":"10.1007\/3-540-44518-8_11"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB21","doi-asserted-by":"crossref","unstructured":"Daniel Kstner. PROPAN: A Retargetable System for Postpass Optimisations and Analyses. In Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers and Tools for Embedded Systems, Vancouver, CA, June 2000.","DOI":"10.1007\/3-540-45245-1_5"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB22","unstructured":"Daniel Kstner. Retargetable Postpass Optimisation by Integer Linear Programming. PhD thesis, Universit\u00e4t des Saarlandes, 2000."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB23","unstructured":"Birger Landwehr. A Genetic Algorithm based Approach for Multi-Objective Data-Flow Graph Optimization. In Asia South Pacific Design Automation Conference (ASP-DAC), Hong Kong, China, January 1999."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB24","doi-asserted-by":"crossref","unstructured":"Rainer Leupers, Johann Elste, and Birger Landwehr. Generation of Interpretive and Compiled Instruction Set Simulators. In ASP-DAC'99, Hong Kong, January 1999.","DOI":"10.1109\/ASPDAC.1999.760028"},{"year":"2001","series-title":"Retargetable Compiler Technology for Embedded Processors","author":"Leupers","key":"10.1016\/S1571-0661(04)80394-3_NEWBIB25"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB26","unstructured":"Thomas M\u00fcller. Effiziente Verfahren zur Befehlsanordnung. PhD thesis, Universit\u00e4t Karlsruhe, jun 1995."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB27","doi-asserted-by":"crossref","unstructured":"George C. Necula. Translation Validation for an Optimizing Compiler. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00), 2000.","DOI":"10.1145\/349299.349314"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB28","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1007\/s002360050099","article-title":"Code generation based on formal BURS theory and heuristic search","volume":"34","author":"Nymeyer","year":"1997","journal-title":"Acta Informatica"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB29","unstructured":"George C. Necula and Peter Lee. Proof-Carrying Code. Technical Report CMU-CS-96-165, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, November 1996."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB30","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. Proof-Carrying Code. In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'97), January 1997.","DOI":"10.1145\/263699.263712"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB31","doi-asserted-by":"crossref","unstructured":"George C. Necula and Peter Lee. The Design and Implementation of a Certifying Compiler. In Proc. PLDI'98, 1998.","DOI":"10.1145\/277650.277752"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB32","unstructured":"Eduardo Pelegri-Llopart. Rewrite Systems, Pattern Matching and Code Generation. Technical Report UCB\/CSD 88\/423, University of California, Berkeley, jun 1988."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB33","unstructured":"Data Book TM-1300 Media Processor, September 2000."},{"issue":"2","key":"10.1016\/S1571-0661(04)80394-3_NEWBIB34","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/s100090050027","article-title":"The code validation tool (cvt.)","volume":"2","author":"Pnueli","year":"1998","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB35","doi-asserted-by":"crossref","unstructured":"A. Pnueli, M. Siegel, and E. Singermann. Translation validation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems, pages 151\u2013166. Springer, Lecture Notes in Computer Science, vol. 1384, 1998.","DOI":"10.1007\/BFb0054170"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB36","unstructured":"Martin Trapp, G\u00f6tz Lindenmaier, and Boris Boesler. Documentation of the Intermediate Representation FIRM. Technical Report 1999-14, Universitt Karlsruhe, Fakultt fr Informatik, Dec 1999."},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB37","doi-asserted-by":"crossref","unstructured":"Martin Trapp. Optimierung objektorientierter Programme. PhD thesis, Universit\u00e4t Karlsruhe, 1999. Published by Springer Verlag, 2001.","DOI":"10.1007\/978-3-642-59502-8"},{"issue":"6","key":"10.1016\/S1571-0661(04)80394-3_NEWBIB38","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/268999.269003","article-title":"Software Reliability via Run-Time Result-Checking","volume":"44","author":"Wasserman","year":"1997","journal-title":"Journal of the ACM"},{"issue":"5","key":"10.1016\/S1571-0661(04)80394-3_NEWBIB39","first-page":"504","article-title":"On the Construction of Correct Compiler Backends: An ASM Approach","volume":"3","author":"Zimmermann","year":"1997","journal-title":"Journal of Universal Computer Science"},{"key":"10.1016\/S1571-0661(04)80394-3_NEWBIB40","unstructured":"L. Zuck, A. Pnueli, and R. Leviathan. Validation of Optimizing Compilers. Technical Report MCS01-12, Faculty of Mathematics and Computer Science, The Weizmann Institute of Science, August 2001."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104803943?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104803943?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:04:08Z","timestamp":1761609848000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104803943"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,4]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,4]]}},"alternative-id":["S1571066104803943"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80394-3","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,4]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Verified Code Generation for Embedded Systems","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80394-3","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}