18 \usetikzlibrary{shapes}

    19 \usetikzlibrary{shadows}

   185 \only<2>{

   186 \begin{textblock}{11}(1,13)

   187 \small

   188 \bl{$P \,\text{says}\, F \vdash Q\,\text{says}\, F\wedge P \,\text{says}\, G $}

   189 \end{textblock}}

   190 \only<3>{

   191 \begin{textblock}{11}(1,13)

   192 \small

   193 \bl{$\underbrace{P \,\text{says}\, F}_{\Gamma} \vdash \underbrace{Q\,\text{says}\, F}_{F_1} \,\wedge

   194         \underbrace{P \,\text{says}\, G}_{F_2} $}

   195 \end{textblock}}

   196 

   199 

   200 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   201 \mode<presentation>{

   202 \begin{frame}[c]

   203 

   204 \begin{center}

   205 \Large

   206 \bl{\infer{\Gamma \vdash F_2}{\Gamma \vdash F_1\Rightarrow F_2 & \Gamma \vdash F_1}}\bigskip\bigskip\bigskip

   207 

   208 \bl{\infer{\Gamma\vdash P\,\text{says}\, F}{\Gamma \vdash F}}

   209 \end{center}

   210 

   211 \end{frame}}

   212 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   213 

   214 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   215 \mode<presentation>{

   216 \begin{frame}[c]

   217 \frametitle{Digression: Proofs in CS}

   218 

   219 Formal proofs in CS sound like science fiction?\pause{} Completely irrelevant!\pause

   220 

   221 \begin{itemize}

   222 \item in 2008, verification of a small C-compiler\medskip 

   223 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)

   224 \begin{itemize}

   225 \item 200k loc of proof

   226 \item 25 - 30 person years

   227 \item found 160 bugs in the C code (144 by the proof)

   228 \end{itemize}

   229 \end{itemize}

   230 

   231 \end{frame}}

   232 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   233 

   234  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   235   \mode<presentation>{

   236   \begin{frame}[c]

   237   \frametitle{}

   238 

   239   \begin{tabular}{c@ {\hspace{2mm}}c}

   240   \\[6mm]

   241   \begin{tabular}{c}

   242   \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

   243   {\footnotesize Bob Harper}\\[-2.5mm]

   244   {\footnotesize (CMU)}

   245   \end{tabular}

   246   \begin{tabular}{c}

   247   \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

   248   {\footnotesize Frank Pfenning}\\[-2.5mm]

   249   {\footnotesize (CMU)}

   250   \end{tabular} &

   251 

   252   \begin{tabular}{p{6cm}}

   253   \raggedright

   254   \color{gray}{published a proof about a specification in a journal (2005),

   255   $\sim$31pages}

   256   \end{tabular}\\

   257 

   258   \pause

   259   \\[0mm]

   260   

   261   \begin{tabular}{c}

   262   \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

   263   {\footnotesize Andrew Appel}\\[-2.5mm]

   264   {\footnotesize (Princeton)}

   265   \end{tabular} &

   266 

   267   \begin{tabular}{p{6cm}}

   268   \raggedright

   269   \color{gray}{relied on their proof in a\\ {\bf security} critical application}

   270   \end{tabular}

   271   \end{tabular}

   272 

   273   \end{frame}}

   274   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   275 

   276   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   277   \mode<presentation>{

   278   \begin{frame}

   279   \frametitle{Proof-Carrying Code}

   280 

   281   \begin{textblock}{10}(2.5,2.2)

   282   \begin{block}{Idea:}

   283   \begin{center}

   284   \begin{tikzpicture}

   285   \draw[help lines,cream] (0,0.2) grid (8,4);

   286   

   287   \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);

   288   \node[anchor=base] at (6.5,2.8) 

   289      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};

   290 

   291   \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);

   292   \node[anchor=base] at (1.5,2.3) 

   293      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};

   294   

   295   \onslide<3->{

   296   \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);

   297   \node[anchor=base,white] at (6.5,1.1) 

   298      {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

   299 

   300   \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};

   301   \onslide<2->{

   302   \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf certificate};

   303   \node at (3.8,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof}};

   304   }

   305 

   306   

   307   \end{tikzpicture}

   308   \end{center}

   309   \end{block}

   310   \end{textblock}

   311 

   312   %\begin{textblock}{15}(2,12)

   313   %\small

   314   %\begin{itemize}

   315   %\item<4-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 

   316   %803 loc in C including 2 library functions)\\[-3mm]

   317   %\item<5-> 167 loc in C implement a type-checker

   318   %\end{itemize}

   319   %\end{textblock}

   320 

   321   \end{frame}}

   322   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   323 

   324  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

   325   \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   326                      draw=black!50, top color=white, bottom color=black!20]

   327   \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   328                      draw=red!70, top color=white, bottom color=red!50!black!20]

   329   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   330   \mode<presentation>{

   331   \begin{frame}<2->[squeeze]

   332   \frametitle{} 

   333   

   334   \begin{columns}

   335   

   336   \begin{column}{0.8\textwidth}

   337   \begin{textblock}{0}(1,2)

   338 

   339   \begin{tikzpicture}

   340   \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

   341   { \&[-10mm] 

   342     \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

   343     \node (proof1) [node1] {\large Proof}; \&

   344     \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

   345     

   346     \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   347     \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

   348     \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

   349     \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   350      

   351     \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   352     \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   353     \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

   354     \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

   355 

   356     \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   357     \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   358     \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

   359     \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   360   };

   361 

   362   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   363   \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

   364   

   365   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}

   366   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

   367 

   368   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}

   369   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}

   370   

   371   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}

   372   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

   373 

   374   \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 

   375   \end{tikzpicture}

   376 

   377   \end{textblock}

   378   \end{column}

   379   \end{columns}

   380 

   381 

   382   \begin{textblock}{3}(12,3.6)

   383   \onslide<4->{

   384   \begin{tikzpicture}

   385   \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

   386   \end{tikzpicture}}

   387   \end{textblock}

   388 

   389   \end{frame}}

   390   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   391      

   392 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   393   \mode<presentation>{

   394   \begin{frame}[c]

   395   \frametitle{Mars Pathfinder Mission 1997}

   396 

   397   \begin{center}

   398   \includegraphics[scale=0.15]{marspath1.png}

   399   \includegraphics[scale=0.16]{marspath3.png}

   400   \includegraphics[scale=0.3]{marsrover.png}

   401   \end{center}

   402   

   403   \begin{itemize}

   404   \item despite NASA's famous testing procedure, the lander crashed frequently on Mars

   405   \item problem was an algorithm not used in the OS

   406   \end{itemize}

   407 

   408   \end{frame}}

   409   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%