| |
|
| \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} |
| |
|
