\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\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: & N7.07 (North Wing, Bush House)\\
  Slides: & KEATS (also home work is there)\\
  \end{tabular}
  \end{center}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     


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

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

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Old-Fashioned Eng.~vs.~CS}
  
  \begin{center}
  \begin{tabular}{@{}cc@{}}
  \begin{tabular}{@{}p{5.2cm}} 
  \includegraphics[scale=0.058]{../pics/towerbridge.jpg}\\ 
  {\bf bridges}: \\
  \raggedright\small
  engineers can ``look'' at a bridge and have a pretty good
  intuition about whether it will hold up or not\\ 
  (redundancy; predictive theory)
  \end{tabular} &
  \begin{tabular}{p{5cm}} 
  \includegraphics[scale=0.265]{../pics/code.jpg}\\
  \raggedright
  {\bf code}: \\
  \raggedright\small
  programmers have very little intuition about their code; 
  often it is too expensive to have redundancy;
  not ``continuous'' 
  \end{tabular}
  \end{tabular}
  \end{center}

  \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

  \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 (protocols, OS, \ldots).

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large{}Mars Pathfinder Mission 1997}

  \begin{center}
  \includegraphics[scale=0.15]{../pics/marspath1.png}
  \includegraphics[scale=0.16]{../pics/marspath3.png}
  \includegraphics[scale=0.3]{../pics/marsrover.png}
  \end{center}
  
  \begin{itemize}
  \item despite NASA's famous testing procedures, the lander crashed frequently on Mars
  \item a scheduling algorithm was not used in the OS
  \end{itemize}

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

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

  \begin{textblock}{11}(1,3)
  \begin{tabular}{@{\hspace{-10mm}}l}
  \begin{tikzpicture}[scale=1.1]
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
  \node at (8,4) {\textcolor{white}{a}};
  
    

  \only<1>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
  }
  \only<2>{
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[fill, blue!50] (3,0) rectangle (5,0.6);
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
  }
  \only<3>{
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[fill, blue!50] (3,0) rectangle (4.5,0.6);
   \draw[fill, blue!50] (5.5,0) rectangle (6,0.6);
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
   \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);
  }
  \only<4>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<5>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (4,0.6);
   \draw[blue!100, fill] (4,3) rectangle (5, 3.6);
  }
  \only<6>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<7>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
  }
  \only<8>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
  }
  \only<9>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
  }
  \only<10>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
  }
  \only<11>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);
   \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);
  }
  \only<12>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);
   \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);
   \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);
   \node [anchor=base] at (6.3, 1.8) {\Large\ldots};
  }
  \only<13>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<14>{
   \node at (2.5,3.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
   \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<15>{
   \node at (2.5,3.9) {\small locked a resource};  
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
   \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); 
  }


  \draw[very thick,->](0,0) -- (8,0);
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
  \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

  \end{tikzpicture}
  \end{tabular}
  \end{textblock}

  \begin{textblock}{0}(2.5,13)%
  \small
  \onslide<3->{
  \begin{bubble}[8cm]%
  Scheduling: You want to avoid that a high 
  priority process is starved indefinitely.
  \end{bubble}}
  \end{textblock}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large Priority Inheritance Scheduling}

  \begin{itemize}
  \item Let a low priority process $L$ temporarily inherit 
    the high priority of $H$ until $L$ leaves the critical 
    section unlocking the resource.\bigskip
  \item Once the resource is unlocked $L$ returns to its original 
    priority level.
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  
  \begin{textblock}{11}(1,3)
  \begin{tabular}{@{\hspace{-10mm}}l}
  \begin{tikzpicture}[scale=1.1]
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
  \node at (8,4) {\textcolor{white}{a}};
  
  \only<1>{
    \draw[fill, blue!50] (1,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
  }
  \only<2>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
  }
  \only<3>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
    \node at (3.5,3.3) {\small $A$};
  }
  \only<4>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
    \node at (3.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (4,3) rectangle (5,3.6);
    \node at (4.5,3.3) {\small $B$};
  }
  \only<5>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,3) rectangle (6,3.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,3.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};
    \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);
  }
  \only<6>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,3.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$}; 
  }
  \only<7>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);
    \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);
  }
  \only<8>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
  }
  \only<9>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
  }
  \only<10>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
  }
  \only<11>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
    \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);
    \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);
  }

  \draw[very thick,->](0,0) -- (8,0);
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
  \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

  \end{tikzpicture}
  \end{tabular}
  \end{textblock}
  
  \begin{textblock}{0}(2.5,13)%
  \small
  \onslide<11>{
  \begin{bubble}[8cm]%
  Scheduling: You want to avoid that a high 
  priority process is staved indefinitely.
  \end{bubble}}
  \end{textblock}


  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large Priority Inheritance Scheduling}

  \begin{itemize}
  \item Let a low priority process $L$ temporarily inherit 
    the high priority of $H$ until $L$ leaves the critical 
    section unlocking the resource.\bigskip
  \item Once the resource is unlocked $L$ returns to its original 
    priority level. \alert{\bf BOGUS}\pause\bigskip
  \item \ldots $L$ needs to switch to the highest 
    \alert{remaining} priority of the threads that it blocks.
  \end{itemize}\bigskip

  \small this error is already known since around 1999

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

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

  \begin{center}
  \includegraphics[scale=0.25]{../pics/p3.jpg}
  \end{center}

   \begin{itemize}
  \item by Rajkumar, 1991
  \item \it ``it resumes the priority it had at the point of entry into the critical 
  section''
  \end{itemize}

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

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

  \begin{center}
  \includegraphics[scale=0.25]{../pics/p2.jpg}
  \end{center}

   \begin{itemize}
  \item by Jane Liu, 2000
  \item {\it ``The job $J_l$ executes at its inherited 
    priority until it releases $R$; at that time, the 
    priority of $J_l$ returns to its priority 
    at the time when it acquires the resource $R$.''}\medskip
  \item \small gives pseudo code and totally bogus data structures  
  \item \small interesting part ``{\it left as an exercise}''
  \end{itemize}

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

  \begin{center}
  \includegraphics[scale=0.15]{../pics/p1.pdf}
  \end{center}

  \begin{itemize}
  \item by Laplante and Ovaska, 2011 (\$113.76)
  \item \it ``when $[$the task$]$ exits the critical section that
        caused the block, it reverts to the priority it had
        when it entered that section'' 
  \end{itemize}

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

  \begin{center}
  \includegraphics[scale=0.25]{../pics/p4.jpg}
  \end{center}

  \begin{itemize}
  \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible)
  \item \it ``Upon releasing the lock, the 
  $[$low-priority$]$ thread will revert to 
  its original priority.''
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
   
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Priority Scheduling}

  \begin{itemize}
  \item a scheduling algorithm that is widely used in real-time operating systems
  \item has been ``proved'' correct by hand in a paper in 1983
  \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
  
  \item we used the corrected algorithm and then {\bf really} proved
    that it is correct
    
  \item we implemented this algorithm in a small OS called PINTOS
    (used for teaching at Stanford)
    
  \item our implementation was much more efficient than their
    reference implementation

  \end{itemize}

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

\begin{frame}[c]
\frametitle{Big Proofs in CS (1)}

Formal proofs in CS sound like science fiction?

\begin{itemize}
\item in 2008, verification of a 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 less buggy 
\end{itemize}
\end{itemize}

\begin{center}
  \includegraphics[scale=0.12]{../pics/compcert.png}
\end{center}

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

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

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
\begin{frame}[c]
\frametitle{Big Proofs in CS (2)}

\begin{itemize}
\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
  \begin{itemize}
  \item used in helicopters and mobile phones
  \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}

\begin{bubble}[10cm]\small
``Real-world operating-system kernel with an end-to-end proof
of implementation correctness and security enforcement''
\end{bubble}\bigskip\pause

unhackable kernel (New Scientists, September 2015)
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
\begin{frame}[c]
\frametitle{Big Proofs in CS (3)}

\begin{itemize}
\item verified TLS implementation\medskip
\item verified compilers (CompCert, CakeML)\medskip
\item verified distributed systems (Verdi)\medskip
\item verified OSes or OS components\\
(seL4, CertiKOS, \ldots)\bigskip\pause
\item Infer static analyser developed by Facebook  
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
\begin{frame}[c]
\frametitle{How Did This Happen?}

Lots of ways!

\begin{itemize}
\item better programming languages
  \begin{itemize}
  \item basic safety guarantees built in
  \item powerful mechanisms for abstraction and modularity
  \end{itemize}
\item better software development methodology
\item stable platforms and frameworks
\item better use of specifications\medskip\\
  \small If you want to build software that works or is secure, 
    it is helpful to know what you mean by ``works'' and by ``is secure''!
\end{itemize}

\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\;\texttt{skip}\;A}}\qquad
  \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}}
  \medskip\\\pause

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

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

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{\large Concrete Example: Sign-Analysis}
\mbox{}\\[-20mm]\mbox{}

\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
         | \meta{Exp} * \meta{Exp}
         | \meta{Exp} = \meta{Exp} 
         | \meta{num}
         | \meta{var}\\
: \meta{Stmt} ::= \meta{label} :
         | \meta{var} := \meta{Exp}
         | \pcode{jmp?} \meta{Exp} \meta{label}
         | \pcode{goto} \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
\end{plstx}}

\begin{textblock}{0}(7.8,2.5)
\small
\begin{bubble}[5.6cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=3mm]
      a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{textblock}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{\large Concrete Example: Sign-Analysis}
\mbox{}\\[-20mm]\mbox{}

\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
         | \meta{Exp} * \meta{Exp}
         | \meta{Exp} = \meta{Exp} 
         | \meta{num}
         | \meta{var}\\
: \meta{Stmt} ::= \meta{label} :
         | \meta{var} := \meta{Exp}
         | \pcode{jmp?} \meta{Exp} \meta{label}
         | \pcode{goto} \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
\end{plstx}}

\begin{textblock}{0}(7.8,3.5)
\small
\begin{bubble}[5.6cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=3mm]
      n := 6
      m1 := 0
      m2 := 1
top:  jmp? n = 0 done
      tmp := m2
      m2 := m1 + m2
      m1 := tmp
      n := n + -1
      goto top
done:
\end{lstlisting}
\end{bubble}
\end{textblock}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{\large Concrete Example: Sign-Analysis}
\mbox{}\\[-20mm]\mbox{}

\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
         | \meta{Exp} * \meta{Exp}
         | \meta{Exp} = \meta{Exp} 
         | \meta{num}
         | \meta{var}\\
: \meta{Stmt} ::= \meta{label} :
         | \meta{var} := \meta{Exp}
         | \pcode{jmp?} \meta{Exp} \meta{label}
         | \pcode{goto} \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
\end{plstx}}

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{Eval: An Interpreter}
\mbox{}\\[-14mm]\mbox{}

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[n]_{env}$ & $\dn$ & $n$\\
$[x]_{env}$ & $\dn$ & $env(x)$\\
$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\
$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\
$[e_1 = e_2]_{env}$ & $\dn$ & 
$\begin{cases}
1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\
0 & \text{otherwise}
\end{cases}$\\
\end{tabular}}
\end{center}

\footnotesize
\begin{lstlisting}[numbers=none,xleftmargin=-5mm]
def eval_exp(e: Exp, env: Env) : Int = e match {
  case Num(n) => n
  case Var(x) => env(x)
  case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env)
  case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env)
  case Equ(e1, e2) => 
    if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0
}
\end{lstlisting}

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\small
A program
\begin{bubble}[6cm]\footnotesize
\begin{lstlisting}[numbers=none,
                   language={},
                   basicstyle=\ttfamily,
                   xleftmargin=1mm]
      a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}

The \emph{snippets} of the program:

\footnotesize
\begin{columns}
\begin{column}[t]{5cm}
\begin{bubble}[4.5cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=1mm]
""    a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}
\begin{column}[t]{5cm}
\begin{bubble}[4.5cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=1mm]
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}
\begin{column}[t]{2cm}
\begin{bubble}[1.1cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=1mm]
done:
\end{lstlisting}
\end{bubble}
\end{column}
\end{columns}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{Eval for Stmts}
\mbox{}\\[-12mm]\mbox{}

Let \bl{$sn$} be the snippets of a program

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\
$[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\
$[x \,\texttt{:=}\, a::rest]_{env}$ & $\dn$ & 
$[rest]_{(env[x:= [a]_{env}])}$\medskip\\
$[\texttt{jmp?}\;b\;l::rest]_{env}$ & $\dn$ & 
$\begin{cases}
[sn(l)]_{env} & \text{if}\quad[b]_{env} = true\\
[rest]_{env}  & \text{otherwise}
\end{cases}$\medskip\\
$[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\
\end{tabular}}
\end{center}\bigskip

Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}

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



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{Eval in Code}

\footnotesize
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
def eval(sn: Snips) : Env = {
  def eval_stmts(sts: Stmts, env: Env) : Env = sts match {
    case Nil => env
    
    case Label(l)::rest => eval_stmts(rest, env)

    case Assign(x, e)::rest => 
      eval_stmts(rest, env + (x -> eval_exp(e, env)))

    case Jmp(b, l)::rest => 
      if (eval_exp(b, env) == 1) eval_stmts(sn(l), env) 
      else eval_stmts(rest, env)

    case Goto(l)::rest => eval_stmts(sn(l), env)
  }

  eval_stmts(sn(""), Map())
}
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{The Idea of Static Analysis}
\small
\mbox{}\bigskip\\

\begin{columns}
\begin{column}{5cm}
\begin{bubble}[4.5cm]\footnotesize
\begin{lstlisting}[numbers=none,
                   language={},
                   basicstyle=\ttfamily,
                   xleftmargin=1mm]
      a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}

\begin{column}{1cm}
\raisebox{-20mm}{\LARGE\bf$\Rightarrow$}
\end{column}
\begin{column}{6cm}
\begin{bubble}[4.7cm]\footnotesize
\begin{lstlisting}[numbers=none,
                   language={},
                   basicstyle=\ttfamily,
                   xleftmargin=1mm,
                   escapeinside={(*}{*)}]
      a := (*\hl{'+'}*)
      n := (*\hl{'+'}*) 
top:  jmp? n = (*\hl{'0'}*) done 
      a := a * n 
      n := n + (*\hl{'-'}*) 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}
\end{columns}\bigskip\bigskip

Replace all constants and variables by either 
\pcode{+}, \pcode{-} or \pcode{0}. What we want to find out
is what the sign of \texttt{a} and \texttt{n} is (they should 
always positive).

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Sign Analysis?}

  
  \begin{columns}
  \begin{column}{3cm}
  \begin{tabular}{cc|l}
  $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{}
  - & - & -\\
  - & 0 & -\\
  - & + & -, 0, +\\
  0 & $x$ & $x$\\
  + & - & -, 0, +\\
  + & 0 & +\\
  + & + & +\\
  \end{tabular}
  \end{column}

  \begin{column}{3cm}
  \begin{tabular}{cc|l}
  $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{}
  - & - & +\\
  - & 0 & 0\\
  - & + & -\\
  0 & $x$ & 0\\
  + & - & -\\
  + & 0 & 0\\
  + & + & +\\
  \end{tabular}
  \end{column}
  \end{columns}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\mbox{}\\[-13mm]\mbox{}

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[n]_{aenv}$ & $\dn$ & 
$\begin{cases}
\{+\} & \text{if}\; n > 0\\
\{-\} & \text{if}\; n < 0\\
\{0\} & \text{if}\; n = 0
\end{cases}$\\
$[x]_{aenv}$ & $\dn$ & $aenv(x)$\\
$[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\
$[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\
$[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\
\end{tabular}}
\end{center}

\scriptsize
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match {
  case Num(0) => Set(Zero)
  case Num(n) if (n < 0) => Set(Neg)
  case Num(n) if (n > 0) => Set(Pos)
  case Var(x) => aenv(x)
  case Plus(e1, e2) => 
    aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv))
  case Times(e1, e2) => 
    atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv))
  case Equ(e1, e2) => Set(Zero, Pos)
}
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{AEval for Stmts}
\mbox{}\\[-12mm]\mbox{}

Let \bl{$sn$} be the snippets of a program

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[\texttt{nil}]_{aenv}$ & $\to$ & $(\texttt{nil},aenv)$\medskip\\
$[\texttt{Label}(l:)::rest]_{aenv}$ & $\to$ & $(rest, aenv)$\medskip\\
$[x \,\texttt{:=}\, e::rest]_{aenv}$ & $\to$ & 
$(rest, aenv[x:= [e]_{aenv}])$\medskip\\
$[\texttt{jmp?}\;e\;l::rest]_{aenv}$ & $\to$ & 
$(sn(l),aenv)$ \textcolor{black}{and} $(rest, aenv)$\medskip\\
$[\texttt{goto}\;l::rest]_{aenv}$ & $\to$ & $(sn(l), aenv)$\\
\end{tabular}}
\end{center}\bigskip

Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}, try to 
reach all \emph{states} you can find (until a fix point is reached).

Check whether there are only $aenv$ in the final states that have 
your property.
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Sign Analysis}

  \begin{itemize}
  \item We want to find out whether \texttt{a} and \texttt{n}
  are always positive?\medskip
  \item After a few optimisations, we can indeed find this out.
  \begin{itemize}
  \item equal signs return only \texttt{+} or \texttt{0}
  \item branch into only one direction if you know
  \item if $x$ is \texttt{+}, then $x + \texttt{-1}$ 
  cannot be negative 
  \end{itemize}\bigskip
  
  \item What is this good for? Well, you do not need 
  underflow checks (in order to prevent buffer-overflow
  attacks). In general this technique is used to make sure 
  keys stay secret.
  \end{itemize}
  
  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Take Home Points}

  \begin{itemize}
  \item While testing is important, it does not show the 
    absence of bugs/vulnerabilities.\medskip
  \item More and more we need (formal) proofs that show
    a program is bug free.\medskip

  \item Static analysis is more and more employed nowadays
    in order to automatically hunt for bugs.
  \end{itemize}
  
  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\end{document}


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