--- res/PP-compiler.tex	2009/06/29 09:28:41	1.13
+++ res/PP-compiler.tex	2009/06/29 09:48:14	1.15
@@ -82,24 +82,24 @@ Most notably are the pioneering approach
 the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There
 is also a rich body of work on the related approaches of
 \emph{translation validation}
-\cite{Pnueli98a,Pnueli98b,Ne-pldi00,\cite{ZaksPnueli08}}, 
+\cite{Pnueli98a,Pnueli98b,Ne-pldi00,ZaksPnueli08}, 
 \emph{certifying compilation} 
 \cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and
 \emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. 
 However, an integratedly verified compiler, which is optimizing and
 ensures non-functional program properties such as on time and space
-ressources required by the compiled program is still
+resources required by the compiled program is still
 missing. Complementary to these approaches are approaches focusing on
 frameworks for verifying compiler optimizations
 \cite{781156,1040335,Kundu+09} or the verification of specific
-compiler optizations, such as the \emph{Lazy Code Motion}
+compiler optimizations, such as the \emph{Lazy Code Motion}
 \cite{TristanLeroy09} or instruction scheduling
 \cite{TristanLeroy08}. By far more ambitious and a grand challenge for
 computing research is Tony Hoare's vision of a \emph{verifying
 compiler} which proves properties of the translated program
 \cite{Hoare03}.
 
-\emph{Resource analysis}, especially worst-case execution time analysis $($WCET$)$} for real-time systems, which are often safety-critical, is a vibrant field of research in academia and industry and of fast growing economical relevance,
+\emph{Resource analysis}, especially worst-case execution time analysis $($WCET$)$ for real-time systems, which are often safety-critical, is a vibrant field of research in academia and industry and of fast growing economical relevance,
 especially in the avionics and automotive industry. A survey on
 state-of-the-art tools and methods for WCET analysis has recently been
 given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the
@@ -170,11 +170,11 @@ Doppler research laboratory {\em compila
 processors} with partners from industry (Infineon, OnDemand
 Microelectronics).
 
-The PP is designed to exploit the synergies of the complementary
-expertise of Jens Knoop on resource-aware program analyses and
-optimizations and their verification and of Andreas Krall on
-compilation techniques for embedded processors. Their complementary
-expertise is essential for the PP.
+The PP is designed to synergetically combine the complementary
+expertises of Jens Knoop on verified resource-aware program analyses
+and optimizations and of Andreas Krall on compilation techniques for
+embedded processors. Their complementary expertise is essential for
+the PP.
 
 
 \subsubsection*{Goals (first 4 years):}
@@ -289,7 +289,7 @@ programmer during source code developmen
 providing hints on resource consumption and (2) the compiler to
 optimize for resource consumption. In our previous work we focused on
 compiler support for
-\emph{worst-case execution time analysis $($WCET$)$} \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. Based on this work and expertise we will extend this research towards 
+\emph{worst-case execution time analysis $($WCET$)$} \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. Based on this work we will extend this research towards 
 other quantitive aspects of resource consumption, especially storage
 usage, towards these two global objectives, using the programming
 environment used there as testbed for implementation
@@ -326,7 +326,7 @@ verification, implementation, and applic
 {\bf Pos} & {\bf Type} & {\bf Description}    & {\bf Duration} \\
 NN1 & PhD & reliable compilation / simulation & 4 years \\
 NN2 & PhD & verified compilation              & 4 years \\
-NN3 & PhD & Resource analysis                 & 4 years \\
+NN3 & PhD & resource analysis                 & 4 years \\
 \hline
 \end{tabular}
 
@@ -364,12 +364,12 @@ safer and robust.
       Links to specification and modeling of timing properties, to execution
       models, hardware and software models.
 \item PP Composition and Predictability in RES Architectures
-      [E182/Puschner]: Links to hard- and software models for time
+      [E182.1/Puschner]: Links to hard- and software models for time
       predictable systems, verification of timing behaviour.
 \item PP Formal Verification for Robustness [E184/Veith]: Links to software
       model-checking and testing of code (on source code and intermediate
       code levels), support for program analysis and transformation.
-\item PP Modeling \& Analysis of Robust Distributed Systems [E182/Schmid]:
+\item PP Modeling \& Analysis of Robust Distributed Systems [E182.2/Schmid]:
       Links to functional and non-functional system requirements,
       distribution, concurrency.
 \end{itemize}