diff -r 3db4970ad0aa -r e33545bb2eba slides/slides09.tex
--- a/slides/slides09.tex	Tue Nov 20 13:37:40 2018 +0000
+++ b/slides/slides09.tex	Tue Nov 27 00:45:26 2018 +0000
@@ -1,16 +1,19 @@
 \documentclass[dvipsnames,14pt,t]{beamer}
 \usepackage{../slides}
 \usepackage{../langs}
+\usepackage{../data}
 \usepackage{../graphics}
 \usepackage{../grammar}
 \usepackage{soul}
-\usepackage{mathpartir}
+
 
-% beamer stuff 
+% beamer stuff
 \renewcommand{\slidecaption}{CFL 09, King's College London}
-\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
+
 
 \begin{document}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{%
@@ -24,53 +27,137 @@
   \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}
+  Office: & N\liningnums{7.07} (North Wing, Bush House)\\
+  Slides: & KEATS (also homework is there)\\
   \end{tabular}
   \end{center}
 
-  \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -82,7 +169,11 @@
   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}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -111,534 +202,22 @@
 
 \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).
+quite general (compiler, 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?
+\frametitle{Can This Be Done?}
 
 \begin{itemize}
-\item in 2008, verification of a C-compiler
+\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 less buggy 
+\item is as good as \texttt{gcc -O1}, but much, much less buggy 
 \end{itemize}
 \end{itemize}
 
@@ -650,723 +229,31 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-% \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)}
+\frametitle{Fuzzy Testing C-Compilers}
 
 \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}
+\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{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)
+\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{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