Universitšt Karlsruhe
Verified Code Generation for Embedded Systems


[1]Sabine Glesner, Rubino Geiß, Boris Boesler, Verified Code Generation for Embedded Systems, In Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), Electronic Notes in Theoretical Computer Science (ENTCS), 5th European Conferences on Theory and Practice of Software (ETAPS 2002),, April 13 2002.


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 e ectively. 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.

[Erzeuge bibTeX Eintrag]




Prof. Sabine Glesner
Dr. Boris Boesler
Dr. Rubino Geiß