--- a/slides07.tex Tue Nov 13 04:50:22 2012 +0000
+++ b/slides07.tex Tue Nov 13 09:05:52 2012 +0000
@@ -15,6 +15,8 @@
\usetikzlibrary{positioning}
\usetikzlibrary{calc}
\usepackage{graphicx}
+\usetikzlibrary{shapes}
+\usetikzlibrary{shadows}
\isabellestyle{rm}
\renewcommand{\isastyle}{\rm}%
@@ -180,9 +182,232 @@
\end{tikzpicture}
\end{center}
+\only<2>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}
+\end{textblock}}
+\only<3>{
+\begin{textblock}{11}(1,13)
+\small
+\bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge
+ \underbrace{P \,\text{says}\, G}_{F_2} $}
+\end{textblock}}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+
+\begin{center}
+\Large
+\bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1\Rightarrow F_2 & \Gamma \vdash F_1}}\bigskip\bigskip\bigskip
+
+\bl{\infer{\Gamma\vdash P\,\text{says}\, F}{\Gamma \vdash F}}
+\end{center}
+
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}[c]
+\frametitle{Digression: Proofs in CS}
+
+Formal proofs in CS sound like science fiction?\pause{} Completely irrelevant!\pause
+
+\begin{itemize}
+\item in 2008, verification of a small C-compiler\medskip
+\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
+\begin{itemize}
+\item 200k loc of proof
+\item 25 - 30 person years
+\item found 160 bugs in the C code (144 by the proof)
+\end{itemize}
+\end{itemize}
+
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+
+ \begin{tabular}{c@ {\hspace{2mm}}c}
+ \\[6mm]
+ \begin{tabular}{c}
+ \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
+ {\footnotesize Bob Harper}\\[-2.5mm]
+ {\footnotesize (CMU)}
+ \end{tabular}
+ \begin{tabular}{c}
+ \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
+ {\footnotesize Frank Pfenning}\\[-2.5mm]
+ {\footnotesize (CMU)}
+ \end{tabular} &
+
+ \begin{tabular}{p{6cm}}
+ \raggedright
+ \color{gray}{published a proof about a specification in a journal (2005),
+ $\sim$31pages}
+ \end{tabular}\\
+
+ \pause
+ \\[0mm]
+
+ \begin{tabular}{c}
+ \includegraphics[scale=0.36]{appel.jpg}\\[-2mm]
+ {\footnotesize Andrew Appel}\\[-2.5mm]
+ {\footnotesize (Princeton)}
+ \end{tabular} &
+
+ \begin{tabular}{p{6cm}}
+ \raggedright
+ \color{gray}{relied on their proof in a\\ {\bf security} critical application}
+ \end{tabular}
+ \end{tabular}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{Proof-Carrying Code}
+
+ \begin{textblock}{10}(2.5,2.2)
+ \begin{block}{Idea:}
+ \begin{center}
+ \begin{tikzpicture}
+ \draw[help lines,cream] (0,0.2) grid (8,4);
+
+ \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
+ \node[anchor=base] at (6.5,2.8)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering user: untrusted code\end{tabular}};
+
+ \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
+ \node[anchor=base] at (1.5,2.3)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering developer ---\\ web server\end{tabular}};
+
+ \onslide<3->{
+ \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
+ \node[anchor=base,white] at (6.5,1.1)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
+
+ \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
+ \onslide<2->{
+ \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate};
+ \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof}};
+ }
+
+
+ \end{tikzpicture}
+ \end{center}
+ \end{block}
+ \end{textblock}
+
+ %\begin{textblock}{15}(2,12)
+ %\small
+ %\begin{itemize}
+ %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions;
+ %803 loc in C including 2 library functions)\\[-3mm]
+ %\item<5-> 167 loc in C implement a type-checker
+ %\end{itemize}
+ %\end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
+ draw=black!50, top color=white, bottom color=black!20]
+ \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
+ draw=red!70, top color=white, bottom color=red!50!black!20]
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<2->[squeeze]
+ \frametitle{}
+
+ \begin{columns}
+
+ \begin{column}{0.8\textwidth}
+ \begin{textblock}{0}(1,2)
+
+ \begin{tikzpicture}
+ \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+ { \&[-10mm]
+ \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+ \node (proof1) [node1] {\large Proof}; \&
+ \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+
+ \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \&
+ \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+ \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+
+ \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+ \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\
+
+ \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+ \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+ };
+
+ \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+
+ \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);}
+ \end{tikzpicture}
+
+ \end{textblock}
+ \end{column}
+ \end{columns}
+
+
+ \begin{textblock}{3}(12,3.6)
+ \onslide<4->{
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Mars Pathfinder Mission 1997}
+
+ \begin{center}
+ \includegraphics[scale=0.15]{marspath1.png}
+ \includegraphics[scale=0.16]{marspath3.png}
+ \includegraphics[scale=0.3]{marsrover.png}
+ \end{center}
+
+ \begin{itemize}
+ \item despite NASA's famous testing procedure, the lander crashed frequently on Mars
+ \item problem was an algorithm not used in the OS
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]