# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1447986204 0
# Node ID a6a6bf32fade6ec2614781bd40ba6958571ee295
# Parent  38e368dc9b1003af67b5dbae08b4e8bf98af7278
updated

diff -r 38e368dc9b10 -r a6a6bf32fade handouts/ho07.pdf
Binary file handouts/ho07.pdf has changed
diff -r 38e368dc9b10 -r a6a6bf32fade handouts/ho07.tex
--- a/handouts/ho07.tex	Wed Nov 18 03:02:28 2015 +0000
+++ b/handouts/ho07.tex	Fri Nov 20 02:23:24 2015 +0000
@@ -630,7 +630,7 @@
 
 
 \begin{figure}[p]
-\lstinputlisting{../progs/test-small.j}
+\lstinputlisting[language=JVMIS]{../progs/test-small.j}
 \caption{Generated code for a test program. This code can be 
 processed by an Java assembler producing a class-file, which
 can be run by the \pcode{java}-program.\label{test}}
diff -r 38e368dc9b10 -r a6a6bf32fade handouts/ho08.pdf
Binary file handouts/ho08.pdf has changed
diff -r 38e368dc9b10 -r a6a6bf32fade handouts/ho08.tex
--- a/handouts/ho08.tex	Wed Nov 18 03:02:28 2015 +0000
+++ b/handouts/ho08.tex	Fri Nov 20 02:23:24 2015 +0000
@@ -132,9 +132,9 @@
 a \pcode{pop}-instruction is needed. 
 
 \begin{lstlisting}[language=JVMIS, numbers=none,mathescape]
-$\textrm{\textit{estimate}}($exp1$)$
+$\textrm{\textit{compile}}($exp1$)$
 pop
-$\textrm{\textit{estimate}}($exp2$)$
+$\textrm{\textit{compile}}($exp2$)$
 \end{lstlisting}
 
 \noindent In effect we ``forget'' about the result the first
@@ -169,7 +169,7 @@
 
 
 \begin{lstlisting}[language=JVMIS, numbers=none,mathescape]
-$\textrm{\textit{estimate}}($1+2$)$
+$\textrm{\textit{compile}}($1+2$)$
 dup
 invokestatic XXX/XXX/write(I)V
 \end{lstlisting}
diff -r 38e368dc9b10 -r a6a6bf32fade slides/slides09.pdf
Binary file slides/slides09.pdf has changed
diff -r 38e368dc9b10 -r a6a6bf32fade slides/slides09.tex
--- a/slides/slides09.tex	Wed Nov 18 03:02:28 2015 +0000
+++ b/slides/slides09.tex	Fri Nov 20 02:23:24 2015 +0000
@@ -62,12 +62,196 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t,fragile]
+\frametitle{Compiling AExps}
+
+For example \bl{$1 + ((2 * 3) + (4 - 3))$}:\medskip
+
+\begin{columns}[T]
+\begin{column}{.3\textwidth}
+\begin{center}
+\bl{\begin{tikzpicture}
+\tikzset{level distance=12mm,sibling distance=4mm}
+\tikzset{edge from parent/.style={draw,very thick}}
\Tree [.$+$ [.$1$ ] [.$+$ [.$*$ $2$ $3$ ] [.$-$ $4$ $3$ ]]]
\end{tikzpicture}}
+\end{center}
+\end{column}
+\begin{column}{.3\textwidth}
+\begin{lstlisting}[language=JVMIS,numbers=none]
+ldc 1 
+ldc 2 
+ldc 3 
+imul 
+ldc 4 
+ldc 3 
+isub 
+iadd 
+iadd
+\end{lstlisting}
+\end{column}
+\end{columns}\bigskip
+
+\small
+Traverse tree in post-order \bl{$\Rightarrow$} code for 
+stack-machine
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling AExps}
+
+\bl{
+\begin{center}
+\begin{tabular}{lcl}
+$\textit{compile}(n, E)$ & $\dn$ & $\pcode{ldc}\;n$\smallskip\\
+$\textit{compile}(a_1 + a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\;\textit{compile}(a_2, E)\;@\; \pcode{iadd}$}\smallskip\\
+$\textit{compile}(a_1 - a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{isub}$}\smallskip\\
+$\textit{compile}(a_1 * a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{imul}$}\smallskip\\
+$\textit{compile}(a_1 \backslash a_2, E)$ & $\dn$\\ 
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{idiv}$}\smallskip\\
+$\textit{compile}(x, E)$ & $\dn$ & $\pcode{iload}\;E(x)$\\
+\end{tabular}
+\end{center}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Ifs}
+
+For example
+
+\begin{lstlisting}[mathescape,numbers=none,language={}]
+if 1 = 1 then x := 2 else y := 3
+\end{lstlisting}
+
+
+\begin{center}
+\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
+   ldc 1
+   ldc 1
+   if_icmpne L_ifelse $\quad\tikz[remember picture] \node (C) {\mbox{}};$
+   ldc 2
+   istore 0
+   goto L_ifend $\quad\tikz[remember picture] \node (A) {\mbox{}};$
+L_ifelse: $\quad\tikz[remember picture] \node[] (D) {\mbox{}};$
+   ldc 3
+   istore 1
+L_ifend: $\quad\tikz[remember picture] \node[] (B) {\mbox{}};$
+\end{lstlisting}
+\end{center}
+
+\begin{tikzpicture}[remember picture,overlay]
  \draw[->,very thick] (A) edge [->,to path={-- ++(10mm,0mm) 
+           -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (B.east);
+  \draw[->,very thick] (C) edge [->,to path={-- ++(10mm,0mm) 
+           -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (D.east);
\end{tikzpicture}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Whiles}
+
+For example
+
+\begin{lstlisting}[mathescape,numbers=none,language={}]
+while x <= 10 do x := x + 1
+\end{lstlisting}
+
+
+\begin{center}
+\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
+L_wbegin: $\quad\tikz[remember picture] \node[] (LB) {\mbox{}};$
+   iload 0
+   ldc 10
+   if_icmpgt L_wend $\quad\tikz[remember picture] \node (LC) {\mbox{}};$
+   iload 0
+   ldc 1
+   iadd
+   istore 0
+   goto L_wbegin $\quad\tikz[remember picture] \node (LA) {\mbox{}};$
+L_wend: $\quad\tikz[remember picture] \node[] (LD) {\mbox{}};$
+\end{lstlisting}
+\end{center}
+
+\begin{tikzpicture}[remember picture,overlay]
+  \draw[->,very thick] (LA) edge [->,to path={-- ++(12mm,0mm) 
+           -- ++(0mm,17.3mm) |- (\tikztotarget)},line width=1mm] (LB.east);
+  \draw[->,very thick] (LC) edge [->,to path={-- ++(12mm,0mm) 
+           -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (LD.east);
\end{tikzpicture}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Writes}
+
+\small
+\begin{lstlisting}[language=JVMIS,mathescape,
+                   numbers=none,xleftmargin=-6mm]
+.method public static write(I)V 
+  .limit locals 1 
+  .limit stack 2 
+  getstatic java/lang/System/out 
+                            Ljava/io/PrintStream; 
+  iload 0
+  invokevirtual java/io/PrintStream/println(I)V 
+  return 
+.end method
+
+
+
+iload $E(x)$ 
+invokestatic XXX/XXX/write(I)V
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Main}
+
+\footnotesize
+\begin{lstlisting}[language=JVMIS,mathescape,
+                   numbers=none,xleftmargin=-6mm]
+.class public XXX.XXX
+.super java/lang/Object
+
+.method public <init>()V
+    aload_0
+    invokenonvirtual java/lang/Object/<init>()V
+    return
+.end method
+
+.method public static main([Ljava/lang/String;)V
+    .limit locals 200
+    .limit stack 200
+
+      $\textit{\ldots{}here comes the compiled code\ldots}$
+
+    return
+.end method
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c,fragile]
 \frametitle{Functional Programming}
 
 \footnotesize
 \begin{textblock}{13}(0.9,3)
-\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
+\begin{lstlisting}[]numbers=none]
 def fib(n) = if n == 0 then 0 
              else if n == 1 then 1 
              else fib(n - 1) + fib(n - 2);
@@ -137,76 +321,16 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Arithmetic Functions}
-
-Compilation of some aritmetic functions:
-
-\begin{center}
-\begin{tabular}{lcl}
-\texttt{Aop("+", a1, a2)} & $\Rightarrow$ & \texttt{...iadd}\\
-\texttt{Aop("-", a1, a2)} & $\Rightarrow$ & \texttt{...isub}\\
-\texttt{Aop("*", a1, a2)} & $\Rightarrow$ & \texttt{...imul}\\
-\texttt{Aop("/", a1, a2)} & $\Rightarrow$ & \texttt{...idiv}\\
-\texttt{Aop("\%", a1, a2)} & $\Rightarrow$ & \texttt{...irem}\\
-\end{tabular}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Boolean Expressions}
-
-Compilation of Boolean expressions:
-
-\begin{center}
-\begin{tikzpicture}[node distance=2mm and 4mm,
- block/.style={rectangle, minimum size=1cm, draw=black, line width=1mm},
- point/.style={rectangle, inner sep=0mm, minimum size=0mm, fill=red},
- skip loop/.style={red, line width=1mm, to path={-- ++(0,-10mm) -| (\tikztotarget)}}]
-\node (A1) [point] {};
-\node (b) [block, right=of A1] {code of \bl{$b$}};
-\node (A2) [point, right=of b] {};
-\node (cs1) [block, right=of A2] {code of \bl{$cs_1$}};
-\node (A3) [point, right=of cs1] {};
-\node (cs2) [block, right=of A3] {code of \bl{$cs_2$}};
-\node (A4) [point, right=of cs2] {};
-
-\only<1>{
-\draw (A1) edge [->, red, line width=1mm] (b);
-\draw (b) edge [->, red, line width=1mm] (A2);
-\draw (A2) edge [skip loop] (A3);
-\draw (A3) edge [->, red, line width=1mm] (cs2);
-\draw (cs2) edge [->,red, line width=1mm] (A4);
-\node [below=of cs1] {\raisebox{-5mm}{\small{}conditional jump}};}
-\end{tikzpicture}
-\end{center}
-
-\begin{center}
-\begin{tabular}{lcl}
-\texttt{Bop("==", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpne...}\\
-\texttt{Bop("!=", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpeq...}\\
-\texttt{Bop("<", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpge...}\\
-\texttt{Bop("<=", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpgt...}\\
-\end{tabular}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c, fragile]
 \frametitle{Sequences}
 
-Compiling \texttt{arg1 ; arg2}:\bigskip
+Compiling \texttt{exp1 ; exp2}:\bigskip
 
 
-\begin{lstlisting}[language=JVMIS, numbers=none]
-...arg1...
+\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
+$\textit{compile}$(exp1)
 pop
-...arg1...
+$\textit{compile}$(exp2)
 \end{lstlisting}
   
 \end{frame}
@@ -216,25 +340,38 @@
 \begin{frame}[c, fragile]
 \frametitle{Write}
 
-Compiling call to \texttt{write(arg)}:\bigskip
+Compiling call to \texttt{write(1+2)}:\bigskip
 
 
-\begin{lstlisting}[language=JVMIS, numbers=none]
-...arg...
+\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
+$\textit{compile}$(1+2)
 dup
 invokestatic XXX/XXX/write(I)V
 \end{lstlisting}\bigskip
 
 \small
-needs a helper function
+needs the helper method
 
+\footnotesize
+\begin{lstlisting}[language=JVMIS, 
+                   xleftmargin=2mm, 
+                   numbers=none]
+.method public static write(I)V 
+   .limit locals 1
+   .limit stack 2
+   getstatic java/lang/System/out Ljava/io/PrintStream; 
+   iload 0 
+   invokevirtual java/io/PrintStream/println(I)V 
+   return 
+.end method
+\end{lstlisting}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
+\begin{frame}[t, fragile]
 \frametitle{Function Definitions}
 
 \footnotesize
@@ -251,12 +388,14 @@
 .end method
 \end{lstlisting}\bigskip
 
-\small We will need for definitions\footnotesize\medskip
+\small We will need for definitions, like\footnotesize\medskip
 
 \begin{lstlisting}[language=JVMIS, 
                    xleftmargin=2mm, 
                    numbers=none]
-.method public static f (I...I)I
+def fname (x1, ... , xn) = ...                   
+                   
+.method public static fname (I...I)I
   .limit locals ??
   .limit stack ?? 
   ??
@@ -269,28 +408,28 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c, fragile]
 \frametitle{Stack Estimation}
-\footnotesize
-\begin{center}
-\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
-def max_stack_exp(e: Exp): Int = e match {
-  case Call(_, args) => args.map(max_stack_exp).sum
-  case If(a, e1, e2) => max_stack_bexp(a) + 
-    (List(max_stack_exp(e1), max_stack_exp(e1)).max)
-  case Write(e) => max_stack_exp(e) + 1
-  case Var(_) => 1
-  case Num(_) => 1
-  case Aop(_, a1, a2) => 
-    max_stack_exp(a1) + max_stack_exp(a2)
-  case Sequ(e1, e2) => 
-    List(max_stack_exp(e1), max_stack_exp(e2)).max
-}
+\small
+\mbox{}\\[-15mm]
 
-def max_stack_bexp(e: BExp): Int = e match {
-  case Bop(_, a1, a2) => 
-    max_stack_exp(a1) + max_stack_exp(a2)
-}
-\end{lstlisting}
-\end{center}
+\bl{\begin{center}
+\begin{tabular}{@{\hspace{-4mm}}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
+$\textit{estimate}(n)$ & $\dn$ & $1$\\
+$\textit{estimate}(x)$ & $\dn$ & $1$\\
+$\textit{estimate}(a_1\;aop\;a_2)$ & $\dn$ &
+$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
+$\textit{estimate}(\pcode{if}\;b\;\pcode{then}\;e_1\;\pcode{else}\;e_2)$ & $\dn$ & 
+$\textit{estimate}(b) +$\\ 
+& & $\quad max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
+$\textit{estimate}(\pcode{write}(e))$ & $\dn$ & 
+$\textit{estimate}(e) + 1$\\
+$\textit{estimate}(e_1 ; e_2)$ & $\dn$ & 
+$max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
+$\textit{estimate}(f(e_1, ..., e_n))$ & $\dn$ & 
+$\sum_{i = 1..n}\;estimate(e_i)$\medskip\\
+$\textit{estimate}(a_1\;bop\;a_2)$ & $\dn$ &
+$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
+\end{tabular}
+\end{center}}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
@@ -304,7 +443,7 @@
 \begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
 .method public static suc(I)I 
 .limit locals 1
-.limit stack 3
+.limit stack 2
   iload 0
   ldc 1
   iadd
@@ -337,7 +476,7 @@
 \begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
 .method public static add(II)I 
 .limit locals 2
-.limit stack 6
+.limit stack 5
   iload 0
   ldc 0
   if_icmpne If_else
@@ -526,173 +665,97 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-\large\bf
-Using a compiler, \\how can you mount the\\ perfect attack against a system?
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-{\large\bf
-What is a \alert{perfect} attack?}\bigskip
-
-\begin{enumerate}
-\item you can potentially completely take over a target system
-\item your attack is (nearly) undetectable
-\item the victim has (almost) no chance to recover
-\end{enumerate}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-
-
-  \begin{center}
-  \begin{tikzpicture}[scale=1]
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{Dijkstra on Testing}
   
-  \onslide<1->{
-  \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=17mm] {};
-  \node [below right] at (A.north west) {\footnotesize\begin{tabular}{@{}l@{}}
-  \only<1,2>{clean}\only<3->{\alert{hacked}}\\compiler\end{tabular}};}
-
-
-  \onslide<2->{
-  \node (B) at (-2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};
-  \node [below right] at (B.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(src)\end{tabular}};
+  \begin{bubble}[10cm]
+  ``Program testing can be a very effective way to show the
+  presence of bugs, but it is hopelessly inadequate for showing
+  their absence.''
+  \end{bubble}\bigskip
   
-  \node (C) at (2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};
-  \node [below right] at (C.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(bin)\end{tabular}};
-
-  \draw[->, line width=2mm] (B) -- (C);
-  }
+  \small
+  What is good about compilers: the either seem to work,
+  or go horribly wrong (most of the time).
   
- \onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};}
-
-  \end{tikzpicture}
-  \end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
 \begin{frame}[c]
+\frametitle{\Large Proving Programs to be Correct}
 
-  \begin{center}
-  \begin{tikzpicture}[scale=1]
-  
-  \onslide<1->{
-  \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
-  \node [below right] at (A.north west) {\small V0.01};
-  \node [below right] (A1) at (A.south west) {\small Scala};
-  \node [below right] (A1) at (A1.south west) {\small\textcolor{gray}{host language}};
-  \node [above right] at (A.north west) {my compiler (src)};}
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} There are infinitely many prime 
+numbers.\medskip\\
 
-  \onslide<2->{
-  \node (B) at (1.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
-  \node [below right] at (B.north west) {\small V0.02};
-  \node [below right] at (B.south west) {\small Scala};
-  \node at (3,0) {\ldots};
+{\bf Proof} \ldots\\
+\end{bubble}\bigskip
 
-  \node (C) at (5,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
-  \node [below right] at (C.north west) {\small V1.00};
-  \node [below right] at (C.south west) {\small Scala};}
+
+similarly\bigskip
 
-  \onslide<3->{
-  \node (D) at (6.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
-  \node [below right] at (D.north west) {\small V1.00};
-
-  \node (E) at (6.8,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
-  \node [below right] at (E.north west) {\small V1.01};}
-  
-  \onslide<4->{
-  \node (F) at (8.6,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
-  \node [below right] at (F.north west) {\small V1.01};
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} The program is doing what 
+it is supposed to be doing.\medskip
 
-  \node (G) at (8.6,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
-  \node [below right] at (G.north west) {\small V1.02};
-  \node at (9.8,0) {\ldots};
-  \node at (9.8,2) {\ldots};
-  \node at (8,-2) {\textcolor{gray}{\begin{tabular}{@{}l@{}}no host language\\needed\end{tabular}}};
-  }
-  
-  \end{tikzpicture}
-  \end{center}
+{\bf Long, long proof} \ldots\\
+\end{bubble}\bigskip\medskip
 
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+\small This can be a gigantic proof. The only hope is to have
+help from the computer. `Program' is here to be understood to be
+quite general (compiler, OS, \ldots).
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}<1-3>
-  \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers 
-  \end{tabular}}
-  
-  %Why is it so paramount to have a small trusted code base (TCB)?
-  \bigskip\bigskip
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+\begin{frame}[c]
+\frametitle{Can This Be Done?}
 
-  \begin{columns}
-  \begin{column}{2.7cm}
-  \begin{minipage}{2.5cm}%
-  \begin{tabular}{c@ {}}
-  \includegraphics[scale=0.2]{../pics/ken-thompson.jpg}\\[-1.8mm]
-  \footnotesize Ken Thompson\\[-1.8mm]
-  \footnotesize Turing Award, 1983\\
-  \end{tabular}
-  \end{minipage}
-  \end{column}
-  \begin{column}{9cm}
-  \begin{tabular}{l@ {\hspace{1mm}}p{8cm}}
- 
-  & Ken Thompson showed how to hide a Trojan Horse in a 
-  compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]
-  
-  & No amount of source level verification will protect 
-  you from such Thompson-hacks.\\[2mm]
+\begin{itemize}
+\item in 2008, verification of a small C-compiler
+\begin{itemize}
+\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
+\item is as good as \texttt{gcc -O1}, but much, much less buggy 
+\end{itemize}
+\end{itemize}
+
+\begin{center}
+  \includegraphics[scale=0.12]{../pics/compcert.png}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
-  & Therefore in safety-critical systems it is important to rely 
-  on only a very small TCB.
-  \end{tabular}
-  \end{column}
-  \end{columns}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+\begin{frame}[c]
+\frametitle{Fuzzy Testing C-Compilers}
+
+\begin{itemize}
+\item tested GCC, LLVM and others by randomly generating 
+C-programs
+\item found more than 300 bugs in GCC and also
+many in LLVM (some of them highest-level critical)\bigskip
+\item about CompCert:
 
-  \only<2>{
-  \begin{textblock}{6}(4,2)
-  \begin{tikzpicture}
-  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
-  {\normalsize
-  \begin{minipage}{8cm}
-  \begin{quote}
-  \includegraphics[scale=0.05]{../pics/evil.png}
-  \begin{enumerate}
-  \item[1)] Assume you ship the compiler as binary and also with sources.
-  \item[2)] Make the compiler aware when it compiles itself.
-  \item[3)] Add the Trojan horse.
-  \item[4)] Compile.
-  \item[5)] Delete Trojan horse from the sources of the compiler.
-  \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}
-  \end{enumerate}
-  \end{quote}
-  \end{minipage}};
-  \end{tikzpicture}
-  \end{textblock}}
+\begin{bubble}[10cm]\small ``The striking thing about our CompCert
+results is that the middle-end bugs we found in all other
+compilers are absent. As of early 2011, the under-development
+version of CompCert is the only compiler we have tested for
+which Csmith cannot find wrong-code errors. This is not for
+lack of trying: we have devoted about six CPU-years to the
+task.'' 
+\end{bubble} 
+\end{itemize}
 
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 \end{document}