Changeset 2587 for Deliverables/Dissemination/proof-structured-traces

Ignore:
Timestamp:
Jan 23, 2013, 1:51:04 PM (7 years ago)
Message:

Tweak talk a little.

Location:
Deliverables/Dissemination/proof-structured-traces
Files:
2 edited

Legend:

Unmodified
 r2585 \footnotesize Project FP7-ICT-2009-C-243881 } \date{23rd January 2013} \date{CerCo workshop, HiPEAC 2013\\23rd January 2013} \maketitle \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, Leroy et al.'s \blue{CompCert}. \bigskip Concentrate on cost correctness. \begin{itemize} \item Keep changes to \alert{extensional} proof minimal \end{itemize} } & \begin{uncoverenv}<3-4> \begin{uncoverenv}<3-5> \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, emph={[2]_cost3},emphstyle={[2]\color{blue}}] \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 Sketched proof for formalised CerCo compiler \bigskip \begin{itemize} \item Preserving trace structure provides correctness in more challenging \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} \end{document} % LocalWords:  LFCS Matita CerCo intensional % LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM % LocalWords:  reexecutes subtrace RTLabs subtraces