| instruction set simulator with modelling of energy consumtion is Wattch |
instruction set simulator with modelling of energy consumtion is Wattch |
| \cite{BrooksTiwariMartonosi00}. |
\cite{BrooksTiwariMartonosi00}. |
| |
|
| Compiler Verification \cite{Hoare,1328444,1314860} |
Compiler Verification |
| |
|
| |
\cite{Hoare03} |
| |
\cite{TristanLeroy09} |
| |
\cite{TristanLeroy08} |
| |
\cite{Kundu+09} |
| |
\cite{Necula00} |
| |
\cite{ZaksPnueli08} |
| |
\cite{Pnueli98a} |
| |
\cite{Pnueli98b} |
| |
\cite{GlesnerGoosZimmeermann04} |
| |
\cite{GoosZimmermann00} |
| |
\cite{BlechPoetzsch07} |
| |
|
| WCET \cite{} |
WCET \cite{} |
| |
|
| |
|
| \paragraph*{WP2 - Verified Compilation} |
\paragraph*{WP2 - Verified Compilation} |
| |
|
| translation verification, specification of semantics of IRs solving |
Suitable semantics are necessary which support efficient translation |
| subproblems. |
validation or support easy verification of a compiler. We will research |
| |
into different semantics and into mappings between the semantics of our |
| |
processor description language \cite{BrEbKr07} and a compiler backend |
| |
semantics, intermediate representation semantics (compatible to LLVM) and |
| |
source language semantics. The main research will be on verification and |
| |
translation validation for all kinds of compiler optimizations. |
| |
|
| |
\begin{itemize} |
| |
\item Evaluate different semantics regarding suitability for compiler |
| |
verification and translation validation, eventually develop new |
| |
semantics |
| |
\item Develop a translator for an automatic mapping from our processor |
| |
description language into verification semantics |
| |
\item Develop a validation system from the intermediate representation |
| |
(LLVM) to the processor semantics |
| |
\item Develop a validation system from the source language (C) to the |
| |
intermediate representation (LLVM) |
| |
\item Research into verification and translation validation for different |
| |
frontend and backend optimizations |
| |
\end{itemize} |
| |
|
| \paragraph*{WP3 - Worst Case Ececution Time Analysis} |
\paragraph*{WP3 - Worst Case Ececution Time Analysis} |
| |
|
