Changeset 2587
- Timestamp:
- Jan 23, 2013, 1:51:04 PM (8 years ago)
- Location:
- Deliverables/Dissemination/proof-structured-traces
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex
r2585 r2587 32 32 \footnotesize Project FP7-ICT-2009-C-243881 33 33 } 34 \date{ 23rd January 2013}34 \date{CerCo workshop, HiPEAC 2013\\23rd January 2013} 35 35 \maketitle 36 36 … … 38 38 \frametitle{Introduction} 39 39 40 The \emph{Matita} proof assistant supports writing and verifi ed functional41 programs.40 The \emph{Matita} proof assistant supports writing and verification of 41 functional programs. 42 42 43 43 \bigskip 44 44 45 45 We 46 47 46 \begin{itemize} 48 47 \item formalise the CerCo compiler in Matita, … … 81 80 Leroy et al.'s \blue{CompCert}. 82 81 82 \bigskip 83 83 Concentrate on cost correctness. 84 \begin{itemize} 85 \item Keep changes to \alert{extensional} proof minimal 86 \end{itemize} 84 87 } 85 88 … … 246 249 & 247 250 248 \begin{uncoverenv}<3- 4>251 \begin{uncoverenv}<3-5> 249 252 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, 250 253 emph={[2]_cost3},emphstyle={[2]\color{blue}}] … … 273 276 \begin{itemize} 274 277 \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 function276 \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> 279 282 \begin{itemize} 280 283 \item Use labels and end of function as measurement points 284 \item All costs are considered local to the function 281 285 \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> 286 289 \begin{itemize} 287 290 \item Use labels and end of function as measurement points … … 468 471 Sketched proof for formalised CerCo compiler 469 472 470 \bigskip471 473 \begin{itemize} 472 474 \item Preserving trace structure provides correctness in more challenging … … 477 479 \item increasing confidence in approach 478 480 \end{itemize} 481 \item[$\star$] Don't need huge changes to existing proofs 482 \end{itemize} 483 484 \pause 485 Future: 486 \begin{itemize} 479 487 \item Expect results to generalise to more general labelling schemes 480 488 \begin{itemize} 481 489 \item hence more sophisticated targets 482 490 \end{itemize} 491 \item Other compiler correctness techniques 492 \begin{itemize} 493 \item Translation validation? 494 \end{itemize} 483 495 \end{itemize} 484 496 … … 487 499 \end{document} 488 500 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.