--- res/PP-compiler.tex	2009/06/28 15:01:57	1.7
+++ res/PP-compiler.tex	2009/06/28 16:53:25	1.9
@@ -70,19 +70,20 @@ in the Handbook of Signal Processing sys
 instruction set simulator with modelling of energy consumtion is Wattch
 \cite{BrooksTiwariMartonosi00}.
 
-Compiler Verification
+Three aspects of program and compiler correctness exist. The verifying
+compiler proves properties of the translated program and is a grand challenge
+for computing research \cite{Hoare03}. A certified compiler like Verfix is
+proven once to do semantically equivalent optimizations and translations
+\cite{GlesnerGoosZimmeermann04,GoosZimmermann00}. Translation validation proves
+at every compiler run that the translation is correct and was introduced by
+Pnueli et al.\ \cite{Pnueli98a,Pnueli98b} and Necula \cite{Necula00}. Until now
+some optimizations have been verified, recently lazy code motion
+\cite{TristanLeroy09}, instruction scheduling \cite{TristanLeroy08}, or the whole
+code generation phase \cite{BlechPoetzsch07}. Another research direction is the
+construction of general frameworks for validation \cite{ZaksPnueli08} or
+generalizations like parameterized equivalence checking \cite{Kundu+09}.
+ 
 
- \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{}
 
@@ -170,8 +171,27 @@ hardware/software and pure software tech
 
 \paragraph*{WP2 - Verified Compilation}
 
-translation verification, specification of semantics of IRs solving
-subproblems.
+Suitable semantics are necessary which support efficient translation
+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}