Changeset 2587

Timestamp:

Jan 23, 2013, 1:51:04 PM (8 years ago)

Author:

campbell

Message:

Tweak talk a little.

Location:

Deliverables/Dissemination/proof-structured-traces

Files:

• proof-structured-traces.pdf (modified) (previous)
• proof-structured-traces.tex (modified) (8 diffs)

Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex

@@ -32 +32 @@
 \footnotesize Project FP7-ICT-2009-C-243881
 }
-\date{23rd January 2013}
+\date{CerCo workshop, HiPEAC 2013\\23rd January 2013}
 \maketitle
 
@@ -38 +38 @@
 \frametitle{Introduction}
 
-The \emph{Matita} proof assistant supports writing and verified functional
-programs.
+The \emph{Matita} proof assistant supports writing and verification of
+functional programs.
 
 \bigskip
 
 We
-
 \begin{itemize}
 \item formalise the CerCo compiler in Matita,
@@ -81 +80 @@
 Leroy et al.'s \blue{CompCert}.
 
+\bigskip
 Concentrate on cost correctness.
+\begin{itemize}
+\item Keep changes to \alert{extensional} proof minimal
+\end{itemize}
 }
 
@@ -246 +249 @@
 &
 
-\begin{uncoverenv}<3-4>
+\begin{uncoverenv}<3-5>
 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
@@ -273 +276 @@
 \begin{itemize}
 \item Use labels and end of function as measurement points
-\item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of whole function
-\end{itemize}
-
-\onslide<3>
+\item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
+\end{itemize}
+
+\onslide<3-4>
 \begin{itemize}
 \item Use labels and end of function as measurement points
+\item All costs are considered local to the function
 \item Actual position of unobservable computation is unimportant
-\item All costs are considered local to the function
-\end{itemize}
-
-\onslide<4>
+\end{itemize}
+
+\onslide<5>
 \begin{itemize}
 \item Use labels and end of function as measurement points
@@ -468 +471 @@
 Sketched proof for formalised CerCo compiler
 
-\bigskip
 \begin{itemize}
 \item Preserving trace structure provides correctness in more challenging
@@ -477 +479 @@
   \item increasing confidence in approach
   \end{itemize}
+\item[$\star$] Don't need huge changes to existing proofs
+\end{itemize}
+
+\pause
+Future:
+\begin{itemize}
 \item Expect results to generalise to more general labelling schemes
   \begin{itemize}
   \item hence more sophisticated targets
   \end{itemize}
+\item Other compiler correctness techniques
+  \begin{itemize}
+  \item Translation validation?
+  \end{itemize}
 \end{itemize}
 
@@ -487 +499 @@
 \end{document}
 
-% LocalWords:  LFCS Matita CerCo intensional
+% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
+% LocalWords:  reexecutes subtrace RTLabs subtraces