### Diff for /res/PP-compiler.tex between versions 1.13 and 1.14

version 1.13, 2009/06/29 09:28:41 version 1.14, 2009/06/29 09:40:11
Line 82  Most notably are the pioneering approach Line 82  Most notably are the pioneering approach
the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There  the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There
is also a rich body of work on the related approaches of  is also a rich body of work on the related approaches of
\emph{translation validation}  \emph{translation validation}
\cite{Pnueli98a,Pnueli98b,Ne-pldi00,\cite{ZaksPnueli08}},   \cite{Pnueli98a,Pnueli98b,Ne-pldi00,ZaksPnueli08},
\emph{certifying compilation}   \emph{certifying compilation}
\cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and  \cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and
\emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}.   \emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}.
However, an integratedly verified compiler, which is optimizing and  However, an integratedly verified compiler, which is optimizing and
ensures non-functional program properties such as on time and space  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  missing. Complementary to these approaches are approaches focusing on
frameworks for verifying compiler optimizations  frameworks for verifying compiler optimizations
\cite{781156,1040335,Kundu+09} or the verification of specific  \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{TristanLeroy09} or instruction scheduling
\cite{TristanLeroy08}. By far more ambitious and a grand challenge for  \cite{TristanLeroy08}. By far more ambitious and a grand challenge for
computing research is Tony Hoare's vision of a \emph{verifying  computing research is Tony Hoare's vision of a \emph{verifying
compiler} which proves properties of the translated program  compiler} which proves properties of the translated program
\cite{Hoare03}.  \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  especially in the avionics and automotive industry. A survey on
state-of-the-art tools and methods for WCET analysis has recently been  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  given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the
Line 289  programmer during source code developmen Line 289  programmer during source code developmen
providing hints on resource consumption and (2) the compiler to  providing hints on resource consumption and (2) the compiler to
optimize for resource consumption. In our previous work we focused on  optimize for resource consumption. In our previous work we focused on
compiler support for  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  other quantitive aspects of resource consumption, especially storage
usage, towards these two global objectives, using the programming  usage, towards these two global objectives, using the programming
environment used there as testbed for implementation  environment used there as testbed for implementation
Line 326  verification, implementation, and applic Line 326  verification, implementation, and applic
{\bf Pos} & {\bf Type} & {\bf Description}    & {\bf Duration} \\  {\bf Pos} & {\bf Type} & {\bf Description}    & {\bf Duration} \\
NN1 & PhD & reliable compilation / simulation & 4 years \\  NN1 & PhD & reliable compilation / simulation & 4 years \\
NN2 & PhD & verified compilation              & 4 years \\  NN2 & PhD & verified compilation              & 4 years \\
NN3 & PhD & Resource analysis                 & 4 years \\  NN3 & PhD & resource analysis                 & 4 years \\
\hline  \hline
\end{tabular}  \end{tabular}

Line 364  safer and robust. Line 364  safer and robust.
Links to specification and modeling of timing properties, to execution        Links to specification and modeling of timing properties, to execution
models, hardware and software models.        models, hardware and software models.
\item PP Composition and Predictability in RES Architectures  \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.        predictable systems, verification of timing behaviour.
\item PP Formal Verification for Robustness [E184/Veith]: Links to software  \item PP Formal Verification for Robustness [E184/Veith]: Links to software
model-checking and testing of code (on source code and intermediate        model-checking and testing of code (on source code and intermediate
code levels), support for program analysis and transformation.        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,        Links to functional and non-functional system requirements,
distribution, concurrency.        distribution, concurrency.
\end{itemize}  \end{itemize}

 Removed from v.1.13 changed lines Added in v.1.14

FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>