Changeset 666 for Deliverables/D1.1/Presentations

Timestamp:

Mar 10, 2011, 1:20:47 PM (9 years ago)

Author:

amadio

Message:

WP-roberto update

File:

• Deliverables/D1.1/Presentations/WP2-roberto.tex (modified) (6 diffs)

Deliverables/D1.1/Presentations/WP2-roberto.tex

@@ -512 +512 @@
 Implement a {\bf proof-of-concept prototype} of the cost annotating compiler.
 
+{\small
 \begin{description}
 
@@ -529 +530 @@
 \item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12). 
 
-\end{description}
+\end{description}}
+
 {\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The
 second part will give more details on Task 2.2, discuss Task 2.3 (with demo), 
@@ -535 +537 @@
 
 \end{frame}
+
+
+
 
 
@@ -562 +567 @@
 
 
-
-
-
-
-
-
-
-
-
-
-
-
-\begin{frame}
-
-\frametitle{Motivation}
-Resource analysis of programming models should, if we are serious about it,
-eventually have an impact on programming practice. Limiting factors include:
-
-\begin{itemize}
-
-\item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.
-
-\item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs.
-
-\item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.
-
-\end{itemize}
-
-\end{frame}
-
-
-\begin{frame}
-
-\frametitle{$\cerco$ goals and approach}
+\begin{frame}
+
+\frametitle{$\cerco$ goals and approach (again)}
 
 \begin{itemize}
@@ -621 +595 @@
 
 
-\begin{frame}
-
-\frametitle{Current technology and our challenge}
-\begin{itemize}
-
-
-\item Compilation phases are heavily {\bf inspected and tested} 
-but not formally checked with a proof assistant.
-\[
-\lustre \arrow \C \arrow \textsc{binary~ code}
-\]
-\item Binary code must be {\bf annotated} with (uncertified) 
-information on the number of iterations of loops.
-
-\item Tools such as \textsc{AbsInt} perform WCET analysis of 
-{\bf sequences of instructions of binary code}.
+
+\begin{frame}
+
+\frametitle{More motivation}
+Resource analysis of programming models should, if we are serious about it,
+eventually have an impact on programming practice. Limiting factors include:
+
+\begin{itemize}
+
+\item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers):  we need an effort to make them concrete and reliable.
+
+\item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs.
+
+\item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with.
 
 \end{itemize}
-
-\noindent \Red{{\bf Our challenge}}
-Lift in a {\em certified way} whathever information we have on the execution
-cost of the binary code to an information on the $\C$ source code (a kind
-of {\bf decompilation}).
 
 \end{frame}
@@ -669 +636 @@
 
 
+\begin{frame}
+
+\frametitle{Current technology and our challenge (again)}
+\begin{itemize}
+
+
+\item Compilation phases are heavily {\bf inspected and tested} 
+but not formally checked with a proof assistant.
+\[
+\lustre \arrow \C \arrow \textsc{binary~ code}
+\]
+\item Binary code must be {\bf annotated} with (uncertified) 
+information on the number of iterations of loops.
+
+\item Tools such as \textsc{AbsInt} perform WCET analysis of 
+{\bf sequences of instructions of binary code}.
+
+\end{itemize}
+
+\noindent \Red{{\bf Our challenge}}
+Lift in a {\em certified way} whathever information we have on the execution
+cost of the binary code to an information on the $\C$ source code (a kind
+of {\bf decompilation}).
+
+\end{frame}
+
+
+
+
 
 \begin{frame}