Changeset 2587


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

Tweak talk a little.

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

Legend:

Unmodified
Added
Removed
  • Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex

    r2585 r2587  
    3232\footnotesize Project FP7-ICT-2009-C-243881
    3333}
    34 \date{23rd January 2013}
     34\date{CerCo workshop, HiPEAC 2013\\23rd January 2013}
    3535\maketitle
    3636
     
    3838\frametitle{Introduction}
    3939
    40 The \emph{Matita} proof assistant supports writing and verified functional
    41 programs.
     40The \emph{Matita} proof assistant supports writing and verification of
     41functional programs.
    4242
    4343\bigskip
    4444
    4545We
    46 
    4746\begin{itemize}
    4847\item formalise the CerCo compiler in Matita,
     
    8180Leroy et al.'s \blue{CompCert}.
    8281
     82\bigskip
    8383Concentrate on cost correctness.
     84\begin{itemize}
     85\item Keep changes to \alert{extensional} proof minimal
     86\end{itemize}
    8487}
    8588
     
    246249&
    247250
    248 \begin{uncoverenv}<3-4>
     251\begin{uncoverenv}<3-5>
    249252\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    250253                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     
    273276\begin{itemize}
    274277\item Use labels and end of function as measurement points
    275 \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of whole function
    276 \end{itemize}
    277 
    278 \onslide<3>
     278\item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
     279\end{itemize}
     280
     281\onslide<3-4>
    279282\begin{itemize}
    280283\item Use labels and end of function as measurement points
     284\item All costs are considered local to the function
    281285\item Actual position of unobservable computation is unimportant
    282 \item All costs are considered local to the function
    283 \end{itemize}
    284 
    285 \onslide<4>
     286\end{itemize}
     287
     288\onslide<5>
    286289\begin{itemize}
    287290\item Use labels and end of function as measurement points
     
    468471Sketched proof for formalised CerCo compiler
    469472
    470 \bigskip
    471473\begin{itemize}
    472474\item Preserving trace structure provides correctness in more challenging
     
    477479  \item increasing confidence in approach
    478480  \end{itemize}
     481\item[$\star$] Don't need huge changes to existing proofs
     482\end{itemize}
     483
     484\pause
     485Future:
     486\begin{itemize}
    479487\item Expect results to generalise to more general labelling schemes
    480488  \begin{itemize}
    481489  \item hence more sophisticated targets
    482490  \end{itemize}
     491\item Other compiler correctness techniques
     492  \begin{itemize}
     493  \item Translation validation?
     494  \end{itemize}
    483495\end{itemize}
    484496
     
    487499\end{document}
    488500
    489 % LocalWords:  LFCS Matita CerCo intensional
     501% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
     502% LocalWords:  reexecutes subtrace RTLabs subtraces
Note: See TracChangeset for help on using the changeset viewer.