\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../data}
\usepackage{../graphics}
\usepackage{../grammar}
\usepackage{soul}
\usepackage{mathpartir}

% beamer stuff
\renewcommand{\slidecaption}{CFL 09, King's College London}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       


\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\[-3mm]
  \LARGE Compilers and \\[-2mm] 
  \LARGE Formal Languages (9)\\[3mm] 
  \end{tabular}}

  \normalsize
  \begin{center}
  \begin{tabular}{ll}
  Email:  & christian.urban at kcl.ac.uk\\
  Office: & N\liningnums{7.07} (North Wing, Bush House)\\
  Slides: & KEATS (also homework is there)\\
  \end{tabular}
  \end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{While Language}
  
\begin{center}
\bl{\begin{tabular}{@{}lcl@{}}
\\[-12mm]        
\meta{Stmt} & $::=$ &  $\texttt{skip}$\\
              & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\
              & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\
              & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\
              & $|$ & \texttt{read}\;\textit{Id}\\
              & $|$ & \texttt{write}\;\textit{Id}\\
              & $|$ & \texttt{write}\;\textit{String}\medskip\\
\meta{Stmts} & $::=$ &  \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$  \meta{Stmt}\medskip\\
\meta{Block} & $::=$ &  \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\
\meta{AExp} & $::=$ & \ldots\\
\meta{BExp} & $::=$ & \ldots\\
\end{tabular}}
\end{center}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}

\mbox{}\\[-18mm]\mbox{}

{\lstset{language=While}\fontsize{10}{12}\selectfont
\texttt{\lstinputlisting{../progs/fib.while}}}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{BF***}

some big array, say \texttt{a}; 7 (8) instructions:

\begin{itemize}
\item \texttt{>} move \texttt{ptr++}
\item \texttt{<} move \texttt{ptr-{}-}
\item \texttt{+} add \texttt{a[ptr]++}
\item \texttt{-} subtract \texttt{a[ptr]-{}-}
\item \texttt{.} print out \texttt{a[ptr]} as ASCII
\item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}
\item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}

\end{itemize}  

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{Arrays in While}

\begin{itemize}
\item \texttt{new arr[15000]}\medskip 
\item \texttt{x := 3 + arr[3 + y]}\medskip 
\item \texttt{arr[42 * n] := ...}
\end{itemize}  

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{New Arrays}

\begin{lstlisting}[mathescape,numbers=none,language=While]
  new arr[number]
\end{lstlisting}\bigskip\bigskip

\begin{lstlisting}[mathescape,numbers=none,language=While]
  ldc number
  newarray int
  astore loc_var
\end{lstlisting}


\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{Array Update}

\begin{lstlisting}[mathescape,numbers=none,language=While]
  arr[...] := 
\end{lstlisting}\bigskip\bigskip

\begin{lstlisting}[mathescape,numbers=none,language=While]
  aload loc_var
  index_aexp
  value_aexp
  iastore
\end{lstlisting}


\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{Array Lookup in AExp}

\begin{lstlisting}[mathescape,numbers=none,language=While]
  ...arr[...]... 
\end{lstlisting}\bigskip\bigskip

\begin{lstlisting}[mathescape,numbers=none,language=While]
  aload loc_var
  index_aexp
  iaload
\end{lstlisting}


\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]
  
  \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}};
  
  \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);
  }
  
 \onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};}

  \end{tikzpicture}
  \end{center}

\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]

  \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)};}

  \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};

  \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};}

  \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};

  \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}

\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{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]

  \end{tabular}
  \end{column}
  \end{columns}

  \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}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.6]{../pics/bridge-limits.png}
  \end{center}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Compilers \& Boeings 777}

First flight in 1994. They want to achieve triple redundancy in hardware
faults.\bigskip

They compile 1 Ada program to\medskip

\begin{itemize}
\item Intel 80486
\item Motorola 68040 (old Macintosh's)
\item AMD 29050 (RISC chips used often in laser printers)
\end{itemize}\medskip

using 3 independent compilers.\bigskip\pause

\small Airbus uses C and static analysers. Recently started using CompCert.

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Goal}

Remember the Bridges example?

\begin{itemize}
\item Can we look at our programs and somehow ensure
they are bug free/correct?\pause\bigskip

\item Very hard: Anything interesting about programs is equivalent
to the Halting Problem, which is undecidable.\pause\bigskip

\item \alert{Solution:} We avoid this ``minor'' obstacle by
      being as close as possible of deciding the halting
      problem, without actually deciding the halting problem.
      \small$\quad\Rightarrow$ yes, no, don't know (static analysis)
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{What is Static Analysis?}

  \begin{center}
  \includegraphics[scale=0.4]{../pics/state.png}
  \end{center}
  
  \begin{itemize}
  \item depending on some initial input, a program 
  (behaviour) will ``develop'' over time.
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{What is Static Analysis?}

  \begin{center}
  \includegraphics[scale=0.4]{../pics/state2.png}
  \end{center}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{What is Static Analysis?}

  \begin{center}
  \includegraphics[scale=0.4]{../pics/state3.jpg}
  \end{center}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{What is Static Analysis?}

  \begin{center}
  \includegraphics[scale=0.4]{../pics/state4.jpg}
  \end{center}

  \begin{itemize}
  \item to be avoided
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{What is Static Analysis?}

  \begin{center}
  \includegraphics[scale=0.4]{../pics/state5.png}
  \end{center}
  
  \begin{itemize}
  \item this needs more work
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{What is Static Analysis?}

  \begin{center}
  \includegraphics[scale=0.4]{../pics/state6.png}
  \end{center}
  
  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c,fragile]
    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
                  Are Vars Definitely Initialised?\end{tabular}}

Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip

Prog.~1:\\
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language=While,xleftmargin=3mm]
if x < 1 then y := x else y := x + 1;
y := y + 1
\end{lstlisting}\medskip     

Prog.~2:\\
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language=While,xleftmargin=3mm]
if x < x then y := y + 1 else y := x;
y := y + 1
\end{lstlisting}            

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c,fragile]
    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
                  Are Vars Definitely Initialised?\end{tabular}}

              What should the rules be for deciding when a
              variable is initialised?\bigskip\pause

\begin{itemize}
\item variable \texttt{x} is definitely initialized after
  \texttt{skip}\\
  iff \texttt{x} is definitely initialized before \texttt{skip}.
\end{itemize}
  
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c,fragile]
%    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
%                  Are Vars Definitely Initialised?\end{tabular}}

$\bl{A}$ is the set of definitely defined variables:
              
\begin{center}
\begin{tabular}{c}
  \bl{\infer{\mbox{}}{A\triangleright\texttt{skip}\triangleright{}A}}\qquad
  \bl{\infer{vars(a) \subseteq A}{A\triangleright
  (\texttt{x\,:=\,a})\triangleright\{x\}\cup A}}
  \medskip\\\pause

  \bl{\infer{A_1\triangleright{}s_1\triangleright{}A_2
  \quad A_2\triangleright{}s_2\triangleright{}A_3}
  {A_1\triangleright{}(s_1 ; s_2)\triangleright{}A_3}}
  \medskip\\\pause
  
  \bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s_1\triangleright{}A_1
  \quad A\triangleright{}s_2\triangleright{}A_2}
  {A\triangleright(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\triangleright{}A_1\cap A_2}}
  \medskip\\\pause

  \bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s\triangleright{}A'}
  {A\triangleright(\texttt{while}\;b\;\texttt{do}\;s)\triangleright{}A}}\pause
\end{tabular}  
\end{center}

\hfill we start with $\bl{A = \{\}}$
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Dijkstra on Testing}
  
  \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
  
  \small
  What is good about compilers: the either seem to work,
  or go horribly wrong (most of the time).
  
  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\Large Proving Programs to be Correct}

\begin{bubble}[10cm]
\small
{\bf Theorem:} There are infinitely many prime 
numbers.\medskip\\

{\bf Proof} \ldots\\
\end{bubble}\bigskip


similarly\bigskip

\begin{bubble}[10cm]
\small
{\bf Theorem:} The program is doing what 
it is supposed to be doing.\medskip

{\bf Long, long proof} \ldots\\
\end{bubble}\bigskip\medskip

\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c]
\frametitle{Can This Be Done?}

\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
\begin{frame}[t]
\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:

\begin{bubble}[10.7cm]\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c]
\frametitle{Next Week}

\begin{itemize}
\item Revision Lecture\medskip
\item How many  strings are in $\bl{L(a^*)}$?\pause\medskip
\item How many  strings are in $\bl{L((a + b)^*)}$?\\ Are there more than
  in $\bl{L(a^*)}$?
\end{itemize}



\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     



\end{document}

%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: