# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1352797552 0
# Node ID 2895a7550754c445b4dc2d464f3a662ad8d9cb18
# Parent  8d3c4efb91b3ba202adcde5090ed7e01eb0f8116
added

diff -r 8d3c4efb91b3 -r 2895a7550754 slides07.pdf
Binary file slides07.pdf has changed
diff -r 8d3c4efb91b3 -r 2895a7550754 slides07.tex
--- 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]