Correct Compilers for Correct Application Specific Processors

A compiler translates a program from a programing language into a program in the machine language of a processor. For embedded systems from the automotive or aerospace domain one important requirement is provable correctness of the translation. Embedded systems often use application specific processors to fulfill performance and efficiency requirements. Within this project techniques and methods to prove correct translations will be developed.

Today safety critical embedded systems are a wide spread technology. However, even minor faults within these systems may lead to heavy damage or even loss of lives. In consequence, correct operation has to be guaranteed in any case.

Many safety critical systems are built upon application specific processors to meet requirements of processing power and energy consumption. Software for these processors is typically written in programming languages like C or C++, and is translated into executable machine code by a compiler. As safety critical systems have to comply to the most rigid quality standards, expensive means of certification are must have.

One quality criterion is that of formal verified semantic equivalence of a programs source code and its binary. Within C3Pro, we aim at the theoretic background and a resulting toolset to enable the generation of correct optimizing compilers and processor simulators. Based on the project's outcome, Catena DSP GmbH will bring these technologies into a market-ready product.

Project Leader
Andreas Krall
Research Group
Dietmar Schreiner
Roland Lezuo
Laura Kovacs
Institut für Computersprachen E185/1
Technische Universität Wien
Argentinierstraße 8/185,
A-1040 Wien, Austria
Tel.: +43 1 58801-18511
Fax: +43 1 58801-18598

The project is funded by the Austrian Research Promotion Agency (FFG) and by Catena DSP GmbH.

Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2010-10-08 (schreiner)