Universität Karlsruhe
Verified Code Generation for Embedded Systems
  author={Sabine Glesner and Rubino Geiß and Boris Boesler},
  title=\{Verified Code Generation for Embedded Systems},
  booktitle=\{In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification)},
  month=\{April 13},
  organization=\{Electronic Notes in Theoretical Computer Science (ENTCS)},
  publisher=\{5th European Conferences on Theory and Practice of Software (ETAPS 2002),},
  abstract=\{Leider nur in Englisch verfĂŒgbar.

Digital signal processors provide specialized SIMD (single instruction multiple data)
operations designed to dramatically increase performance in embedded systems.
While these operations are simple to understand, their unusual functions and their
parallelism make it dicult for automatic code generation algorithms to use them
eectively. In this paper, we present a new optimizing code generation method that
can deploy these operations successfully while also verifying that the generated code
is a correct translation of the input program.

}, url=\{http://www.info.uni-karlsruhe.de/~glesner/my_papers/cocv-02.pdf}, }