source: Deliverables/Dissemination/front-end/final-review/front-end.vrb @ 3278

Last change on this file since 3278 was 3278, checked in by Ian Stark, 7 years ago

Renaming and moving

File size: 394 bytes
Line 
1\frametitle {Putting the proof together}
2
3\begin{center}
4\includegraphics[width=0.8\linewidth]{compiler.pdf}
5\end{center}
6
7\begin{itemize}
8\item `Clock' difference in Clight is sum of cost labels
9\item Observables, including trace of labels, is preserved to ASM
10\item Labelling at bottom level is sound and precise
11\item Sum of labels at ASM is equal to difference in real clock
12\end{itemize}
13
Note: See TracBrowser for help on using the repository browser.