--- res/PP-compiler.tex	2009/06/28 16:26:25	1.8
+++ 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{}