<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">
diff -r 6a43ea9305ba -r 1fe44fb6d0a4 Slides/slides01.tex
--- a/Slides/slides01.tex	Sat Mar 19 23:27:29 2016 +0000
+++ b/Slides/slides01.tex	Thu Mar 31 16:50:37 2016 +0100
@@ -1,28 +1,61 @@
-\documentclass[dvipsnames,14pt,t, xelatex]{beamer}
+\documentclass[dvipsnames,14pt,t]{beamer}
 \usepackage{slides}
+\usepackage{langs}
 \usepackage{graph}
-
+%\usepackage{grammar}
+\usepackage{soul}
+\usepackage{data}
+\usepackage{proof}
 
 % beamer stuff 
-\renewcommand{\slidecaption}{SEN 09, King's College London}
+\renewcommand{\slidecaption}{Canterbury, 22.2.2016}
 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
 
+\newcommand\grid[1]{%
+\begin{tikzpicture}[baseline=(char.base)]
+  \path[use as bounding box]
+    (0,0) rectangle (1em,1em);
+  \draw[red!50, fill=red!20]
+    (0,0) rectangle (1em,1em);
+  \node[inner sep=1pt,anchor=base west]
+    (char) at (0em,\gridraiseamount) {#1};
+\end{tikzpicture}}
+\newcommand\gridraiseamount{0.12em}
+
+\makeatletter
+\newcommand\Grid[1]{%
+  \@tfor\z:=#1\do{\grid{\z}}}
+\makeatother	
+
+\newcommand\Vspace[1][.3em]{%
+  \mbox{\kern.06em\vrule height.3ex}%
+  \vbox{\hrule width#1}%
+  \hbox{\vrule height.3ex}}
+
+\def\VS{\Vspace[0.6em]}
+
+
+
 \begin{document}
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{%
   \begin{tabular}{@ {}c@ {}}
   \\
-  \LARGE Security Engineering (9)\\[-3mm] 
+  \Large POSIX Lexing with Derivatives\\[-1.5mm] 
+  \Large of Regular Expressions\\[-1mm] 
+  %\normalsize Or, How to Find Bugs with the\\[-5mm] 
+  %\normalsize Isabelle Theorem Prover
   \end{tabular}}\bigskip\bigskip\bigskip
 
   \normalsize
   \begin{center}
-  \begin{tabular}{ll}
-  Email:  &amp; christian.urban at kcl.ac.uk\\
-  Office: &amp; S1.27 (1st floor Strand Building)\\
-  Slides: &amp; KEATS (also homework is there)\\
+  \begin{tabular}{c}
+  \small Christian Urban\\
+  \small King's College London\\
+  \\
+  \\
+  Joint work with Fahad Ausaf and Roy Dyckhoff
   \end{tabular}
   \end{center}
 
@@ -33,130 +66,354 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.6]{pics/bridge-limits.png}
+  \includegraphics[scale=0.2]{isabelle.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} &amp;
-  \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}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mbox{}\\[-20mm]\mbox{}
 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Trusting Computing Base}
-  
-When considering whether a system meets some security
-objectives, it is important to consider which parts of that
-system are trusted in order to meet that objective (TCB).
-\bigskip\pause
-
-The smaller the TCB, the less effort it takes to get
-some confidence that it is trustworthy, by doing a code 
-review or by performing some (penetration) testing.
-\bigskip
-
-\footnotesize
-CPU, compiler, libraries, OS, NP $\not=$ P,
-random number generator, \ldots
-\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
-  
-  unfortunately attackers exploit bugs (Satan's computer vs 
-  Murphy's)
+  \begin{itemize}
+  \item Isabelle interactive theorem prover; 
+  some proofs are automatic -- most however need help
+  \item the learning curve is steep; you often have to fight the 
+  theorem prover\ldots no different in other ITPs
+  \end{itemize}
 
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
-\frametitle{\Large Proving Programs to be Correct}
+\frametitle{Why Bother?}
+
+Surely regular expressions must have been implemented and 
+studied to death, no?
 
-\begin{bubble}[10cm]
-\small
-{\bf Theorem:} There are infinitely many prime 
-numbers.\medskip\\
+\begin{center}
+\begin{tikzpicture}
+\begin{axis}[
+    xlabel={{\tt a}s},
+    ylabel={time in secs},
+    enlargelimits=false,
+    xtick={0,5,...,30},
+    xmax=30,
+    ymax=35,
+    ytick={0,5,...,30},
+    scaled ticks=false,
+    axis lines=left,
+    width=8cm,
+    height=6cm, 
+    legend entries={Python,Ruby},  
+    legend pos=north west,
+    legend cell align=left  
+]
+\addplot[blue,mark=*, mark options={fill=white}] 
+  table {re-python.data};
+\addplot[brown,mark=pentagon*, mark options={fill=white}] 
+  table {re-ruby.data};  
+\end{axis}
+\end{tikzpicture}
+\end{center}
 
-{\bf Proof} \ldots\\
-\end{bubble}\bigskip
+evil regular expressions: \bl{$({\tt a}?)^n \cdot {\tt a}^n$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
 
-similarly\bigskip
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\Large Isabelle Theorem Prover}
 
-\begin{bubble}[10cm]
-\small
-{\bf Theorem:} The program is doing what 
-it is supposed to be doing.\medskip
+\begin{itemize}
+\item started to use Isabelle after my PhD (in 2000)
 
-{\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).
+\item the thesis included a rather complicated 
+  ``pencil-and-paper'' proof for a 
+  termination argument (sort of $\lambda$-calculus)\medskip
+ 
+\item me, my supervisor, the examiners did not find any problems\medskip 
+ \begin{center}
+  \begin{tabular}{@ {}c@ {}}
+  \includegraphics[scale=0.38]{barendregt.jpg}\\[-2mm]
+  \footnotesize Henk Barendregt
+  \end{tabular}
+  \hspace{2mm}
+  \begin{tabular}{@ {}c@ {}}
+  \includegraphics[scale=0.20]{andrewpitts.jpg}\\[-2mm]
+  \footnotesize Andrew Pitts
+  \end{tabular}
+  \end{center}
+  
+\item people were building their work on my result      
+  
+\end{itemize}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \begin{frame}[c]
-  \frametitle{\Large{}Mars Pathfinder Mission 1997}
+\begin{frame}[t]
+\frametitle{\Large Nominal Isabelle}
+
+\begin{itemize}
+\item implemented a package for the Isabelle prover 
+in order to reason conveniently about binders 
+ 
+\begin{center}
+\large\bl{$\lambda \alert{x}.\,M$} \hspace{10mm}
+\bl{$\forall \alert{x}.\,P\,x$}
+\end{center}\bigskip\bigskip\bigskip\bigskip
+\bigskip\bigskip\bigskip\pause\pause
+  
+  
+\item when finally being able to formalise the proof from my PhD, I found that the main result
+      (termination) is correct, but a central lemma needed to
+      be generalised
+\end{itemize}
+
+\only&lt;2-&gt;{
+\begin{textblock}{3}(13,5)
+\includegraphics[scale=0.33]{skeleton.jpg}
+\end{textblock}}
+
+\begin{textblock}{3}(5.3,7)
+\onslide&lt;1-&gt;{
+\begin{tikzpicture}
+\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=red]{\mbox{a}};
+\end{tikzpicture}}
+\end{textblock}
+
+\begin{textblock}{3}(8.7,7)
+\onslide&lt;1-&gt;{
+\begin{tikzpicture}
+\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=red]{\mbox{a}};
+\end{tikzpicture}}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\Large Variable Convention}
+
+
+\begin{center}
+\begin{bubble}[10cm]
+  \color{gray}  
+  \small
+  {\bf\mbox{}Variable Convention:}\\[1mm] 
+  If $M_1,\ldots,M_n$ occur in a certain mathematical context
+  (e.g. definition, proof), then in these terms all bound variables 
+  are chosen to be different from the free variables.\\[2mm]
+  
+  \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
+\end{bubble}
+\end{center}
+
+\mbox{}\\[-8mm]
+\begin{itemize}
+
+
+\item instead of proving a property for \alert{\bf all} bound
+variables, you prove it only for \alert{\bf some}\ldots?
+
+\item feels like it is used in 90\% of papers in PT and FP
+(9.9\% use de-Bruijn indices)
+
+\item this is mostly OK, but in some corner-cases you can use it
+to prove \alert{\bf false}\ldots we fixed this!
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+\begin{frame}[c]
+\frametitle{}
+
+\begin{tabular}{c@ {\hspace{2mm}}c}
+\\[6mm]
+\begin{tabular}{c}
+\includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
+{\footnotesize Bob Harper}\\[-2mm]
+{\footnotesize}
+\end{tabular}
+\begin{tabular}{c}
+\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
+{\footnotesize Frank Pfenning}\\[-2mm]
+{\footnotesize}
+\end{tabular} &amp;
+
+\begin{tabular}{p{6cm}}
+\raggedright
+{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,
+$\sim$31pp}
+\end{tabular}\\
+
+\\[0mm]
+  
+\begin{tabular}{c}
+\includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
+{\footnotesize Andrew Appel}\\[-2.5mm]
+{\footnotesize}
+\end{tabular} &amp;
+
+\begin{tabular}{p{6cm}}
+\raggedright
+{relied on their proof in a\\ {\bf security} critical application}
+\end{tabular}
+\end{tabular}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-  \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{frame}
+\frametitle{Proof-Carrying Code}
+
+\begin{textblock}{10}(2.5,2.2)
+\begin{block}{Idea:}
+\begin{center}
+\begin{tikzpicture}
+\draw[help lines,cream] (0,0.2) grid (8,4);
+  
+\draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
+\node[anchor=base] at (6.5,2.8) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};
+
+\draw[line width=1mm, red] (0.1,0.6) rectangle (2.1,4);
+  \node[anchor=base] at (1.1,2.3) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};
+  
+\onslide&lt;3-&gt;{
+  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
+  \node[anchor=base,white] at (6.5,1.1) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
+
+  \node at (3.6,3.0) [single arrow, fill=red,text=white, 
+                      minimum height=3.4cm]{\bf code};
+  \onslide&lt;2-&gt;{
+  \node at (3.6,1.3) [single arrow, fill=red,text=white, 
+                      minimum height=3.4cm]{\bf certificate};
+  \node at (3.6,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof in LF}};
+}
+
+  
+\end{tikzpicture}
+\end{center}
+\end{block}
+\end{textblock}
+
+\begin{textblock}{15}(2,12)
+\small
+\begin{itemize}
+\item&lt;3-&gt; Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 
+803 loc in C including 2 library functions)\\[-3mm]
+\item&lt;3-&gt; 167 loc in C implement a type-checker
+\end{itemize}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}&lt;2-&gt;[squeeze]
+  \frametitle{} 
+  
+  \begin{columns}
+  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
+                     draw=black!50, top color=white, bottom color=black!20]
+  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
+                     draw=red!70, top color=white, bottom color=red!50!black!20]
   
-  \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}
+  \begin{column}{0.8\textwidth}
+  \begin{textblock}{0}(1,2)
+
+  \begin{tikzpicture}
+  \matrix[ampersand replacement=\&amp;,column sep=7mm, row sep=5mm]
+  { \&amp;[-10mm] 
+    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&amp;
+    \node (proof1) [node1] {\large Proof}; \&amp;
+    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+    
+    \onslide&lt;4-&gt;{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&amp;
+    \onslide&lt;4-&gt;{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&amp;
+    \onslide&lt;4-&gt;{\node (proof2) [node1] {\large Proof};} \&amp;
+    \onslide&lt;4-&gt;{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+     
+    \onslide&lt;5-&gt;{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&amp;
+    \onslide&lt;5-&gt;{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&amp;
+    \onslide&lt;5-&gt;{\node (proof3) [node1] {\large Proof};} \&amp;
+    \onslide&lt;5-&gt;{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\
+
+    \onslide&lt;6-&gt;{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&amp;
+    \onslide&lt;6-&gt;{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&amp;
+    \onslide&lt;6-&gt;{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&amp;
+    \onslide&lt;6-&gt;{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+  };
+
+  \draw[-&gt;,black!50,line width=2mm] (proof1) -- (def1);
+  \draw[-&gt;,black!50,line width=2mm] (proof1) -- (alg1);
+  
+  \onslide&lt;4-&gt;{\draw[-&gt;,black!50,line width=2mm] (proof2) -- (def2);}
+  \onslide&lt;4-&gt;{\draw[-&gt;,black!50,line width=2mm] (proof2) -- (alg2);}
+
+  \onslide&lt;5-&gt;{\draw[-&gt;,black!50,line width=2mm] (proof3) -- (def3);}
+  \onslide&lt;5-&gt;{\draw[-&gt;,black!50,line width=2mm] (proof3) -- (alg3);}
+  
+  \onslide&lt;6-&gt;{\draw[-&gt;,black!50,line width=2mm] (proof4) -- (def4);}
+  \onslide&lt;6-&gt;{\draw[-&gt;,black!50,line width=2mm] (proof4) -- (alg4);}
+
+  \onslide&lt;3-&gt;{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
+  \end{tikzpicture}
+
+  \end{textblock}
+  \end{column}
+  \end{columns}
+
+
+  \begin{textblock}{3}(12,3.6)
+  \onslide&lt;4-&gt;{
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+  \end{tikzpicture}}
+  \end{textblock}
+  
+  \begin{textblock}{0}(0.4,12.8)
+  \onslide&lt;6-&gt;{
+  \begin{bubble}[11cm]
+  \small Each time one needs to check $\sim$31pp~of 
+  informal paper proofs.
+  You have to be able to keep definitions 
+  and proofs consistent.
+  \end{bubble}}
+  \end{textblock}
 
   \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%  \begin{frame}[c]
+%  \frametitle{\Large Lessons Learned}
+%
+%  \begin{itemize}
+%  \item using a theorem prover we were able to keep a large 
+%  proof consistent with changes in the definitions\bigskip
+%  \item it took us some 10 days to get to the error\ldots
+%  probably the same time Harper and Pfenning needed to \LaTeX{}
+%  their paper\bigskip 
+%  \item once there, we ran circles around them
+%  \end{itemize}
+%
+%  \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
-  
+  \frametitle{Real-Time Scheduling} 
 
   \begin{textblock}{11}(1,3)
   \begin{tabular}{@{\hspace{-10mm}}l}
@@ -165,7 +422,6 @@
   \node at (8,4) {\textcolor{white}{a}};
   
     
-
   \only&lt;1&gt;{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
   }
@@ -182,33 +438,33 @@
    \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);
   }
   \only&lt;4&gt;{
-   \node at (2.5,0.9) {\small locked a resource};
+   \node at (2.5,0.9) {\small locks 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, &lt;-, line width = 2mm] (2,-0.1) -- (2, -1);
   }
   \only&lt;5&gt;{
-   \node at (2.5,0.9) {\small locked a resource};
+   \node at (2.5,0.9) {\small locks a resource};
    \draw[fill, blue!50] (1,0) rectangle (4,0.6);
    \draw[blue!100, fill] (4,3) rectangle (5, 3.6);
   }
   \only&lt;6&gt;{
-   \node at (2.5,0.9) {\small locked a resource};
+   \node at (2.5,0.9) {\small locks 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, &lt;-, line width = 2mm] (2,-0.1) -- (2, -1);
   }
   \only&lt;7&gt;{
-   \node at (2.5,0.9) {\small locked a resource};
+   \node at (2.5,0.9) {\small locks 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, &lt;-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
   }
   \only&lt;8&gt;{
-   \node at (2.5,0.9) {\small locked a resource}; 
+   \node at (2.5,0.9) {\small locks 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);
@@ -217,7 +473,7 @@
    \draw[red, &lt;-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
   }
   \only&lt;9&gt;{
-   \node at (2.5,0.9) {\small locked a resource}; 
+   \node at (2.5,0.9) {\small locks 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);
@@ -225,7 +481,7 @@
    \draw[red, &lt;-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
   }
   \only&lt;10&gt;{
-   \node at (2.5,0.9) {\small locked a resource}; 
+   \node at (2.5,0.9) {\small locks 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);
@@ -234,7 +490,7 @@
    \draw[red, &lt;-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
   }
   \only&lt;11&gt;{
-   \node at (2.5,0.9) {\small locked a resource};
+   \node at (2.5,0.9) {\small locks 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);
@@ -243,7 +499,7 @@
    \draw[red, &lt;-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);
   }
   \only&lt;12&gt;{
-   \node at (2.5,0.9) {\small locked a resource}; 
+   \node at (2.5,0.9) {\small locks 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);
@@ -254,14 +510,14 @@
    \node [anchor=base] at (6.3, 1.8) {\Large\ldots};
   }
   \only&lt;13&gt;{
-   \node at (2.5,0.9) {\small locked a resource}; 
+   \node at (2.5,0.9) {\small locks 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, &lt;-, line width = 2mm] (2,-0.1) -- (2, -1);
   }
   \only&lt;14&gt;{
-   \node at (2.5,3.9) {\small locked a resource}; 
+   \node at (2.5,3.9) {\small locks 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);
@@ -269,7 +525,7 @@
    \draw[red, &lt;-, line width = 2mm] (2,-0.1) -- (2, -1);
   }
   \only&lt;15&gt;{
-   \node at (2.5,3.9) {\small locked a resource};  
+   \node at (2.5,3.9) {\small locks 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);
@@ -293,8 +549,8 @@
   \small
   \onslide&lt;3-&gt;{
   \begin{bubble}[8cm]%
-  Scheduling: You want to avoid that a high 
-  priority process is starved indefinitely.
+  RT-Scheduling: You want to avoid that a 
+  high-priority process is starved indefinitely.
   \end{bubble}}
   \end{textblock}
 
@@ -306,11 +562,21 @@
   \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 
+  \item Let a low priority process \bl{$L$} temporarily inherit 
+    the high priority of \bl{$H$} until \bl{$L$} leaves the critical 
     section unlocking the resource.\bigskip
-  \item Once the resource is unlocked $L$ returns to its original 
-    priority level.
+  \item Once the resource is unlocked, \bl{$L$} ``returns to its original 
+    priority level.''\\
+    \mbox{}\hfill\footnotesize
+    \begin{tabular}{p{6cm}@{}}
+    L.~Sha, R.~Rajkumar, and J.~P.~Lehoczky. 
+    {\it Priority Inheritance Protocols: An Approach to 
+    Real-Time Synchronization}. IEEE Transactions on 
+    Computers, 39(9):1175â€“1185, 1990
+    \end{tabular}\bigskip\normalsize\pause
+  
+  \item Proved correct, reviewed in a respectable journal....what could possibly be wrong?
+    
   \end{itemize}
 
   \end{frame}
@@ -318,7 +584,7 @@
   
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
-  
+
   \begin{textblock}{11}(1,3)
   \begin{tabular}{@{\hspace{-10mm}}l}
   \begin{tikzpicture}[scale=1.1]
@@ -525,7 +791,7 @@
   \onslide&lt;11&gt;{
   \begin{bubble}[8cm]%
   Scheduling: You want to avoid that a high 
-  priority process is staved indefinitely.
+  priority process is starved indefinitely.
   \end{bubble}}
   \end{textblock}
 
@@ -538,13 +804,13 @@
   \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 
+  \item Let a low priority process \bl{$L$} temporarily inherit 
+    the high priority of \bl{$H$} until \bl{$L$} leaves the critical 
     section unlocking the resource.\bigskip
-  \item Once the resource is unlocked $L$ returns to its original 
+  \item Once the resource is unlocked, \bl{$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.
+  \item \ldots \bl{$L$} needs to switch to the highest 
+    \alert{\bf remaining} priority of the threads that it blocks.
   \end{itemize}\bigskip
 
   \small this error is already known since around 1999
@@ -556,7 +822,7 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.25]{pics/p3.jpg}
+  \includegraphics[scale=0.25]{p3.jpg}
   \end{center}
 
    \begin{itemize}
@@ -568,12 +834,11 @@
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
      
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.25]{pics/p2.jpg}
+  \includegraphics[scale=0.25]{p2.jpg}
   \end{center}
 
    \begin{itemize}
@@ -583,7 +848,7 @@
     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}''
+  \item \small interesting part is ``{\it left as an exercise}''
   \end{itemize}
 
   \end{frame}
@@ -593,7 +858,7 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.15]{pics/p1.pdf}
+  \includegraphics[scale=0.15]{p1.pdf}
   \end{center}
 
   \begin{itemize}
@@ -610,19 +875,19 @@
   \begin{frame}[c]
 
   \begin{center}
-  \includegraphics[scale=0.25]{pics/p4.jpg}
+  \includegraphics[scale=0.22]{p5.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.''
+  \item by Silberschatz, Galvin and Gagne (9th edition, 2013)
+  \item \it ``Upon releasing the
+  lock, the $[$low-priority$]$ thread will revert to its original
+  priority.''
   \end{itemize}
 
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
-   
+    
   
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
@@ -630,201 +895,629 @@
 
   \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 has been ``proved'' correct by hand in a paper in 1990
   \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
   
-  \item we corrected the algorithm and then {\bf really} proved that it is correct	
+  \item we (generalised) the 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
+  \item our implementation was faster than their reference implementation
   \end{itemize}
 
   \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
    
-   
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \begin{frame}[c]
-  \frametitle{Design of AC-Policies}
-
-  Imagine you set up an access policy (root, lpd, users, staff, etc)
-  \bigskip\pause
-
-  \Large
-  \begin{quote}
-  ``what you specify is what you get but not necessarily what you want\ldots''
-  \end{quote}\bigskip\bigskip\bigskip
-  
-  \normalsize main work by Chunhan Wu (a PhD-student in Nanjing)
-
-  \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+%  \begin{frame}[c]
+%  \frametitle{\Large{}Mars Pathfinder Mission 1997}
+%
+%  \begin{center}
+%  \includegraphics[scale=0.15]{marspath1.png}
+%  \includegraphics[scale=0.16]{marspath3.png}
+%  \includegraphics[scale=0.3]{marsrover.png}
+%  \end{center}
+%  
+%  \begin{itemize}
+%  \item despite NASA's famous testing procedures, the lander crashed frequently on Mars
+%  \item a scheduling algorithm was not used in the OS at the 
+%  beginning; PIP was enabled after the cause was identified
+%  \end{itemize}
+%
+%  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
-  \frametitle{Testing Policies}
-
-  \begin{center}
-  \begin{tikzpicture}[scale=1]
-  %\draw[black!10,step=2mm] (-5,-3) grid (5,4);
-  %\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4);
-  \draw[white,thick,step=10mm] (-5,-3) grid (5,4);
-
-  \draw [black!20, line width=1mm] (0,0) circle (1cm);
-  \draw [line width=1mm] (0,0) circle (3cm);
-  \node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};
-  
-  \draw [red, line width=2mm, &lt;-] (-2.1,2.1) -- (-3.5,3.2);
-  \node at (-3.5,3.6) {your system};
-  \node at (-4.8,0) {\Large policy $+$};
-
-  
-  \only&lt;2&gt;{
-  \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);
-  \draw [red, line width=2mm, &lt;-] (2.3,1.2) -- (3.5,2);
-  \node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};}
-
-  \only&lt;3&gt;{
-  \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);
-  \node[white] at (2,1) {\small tainted};}
+  \frametitle{Lessons Learned}
 
-  \only&lt;4&gt;{
-  \begin{scope}
-  \draw [clip] (0,0) circle (2.955cm);
-  \draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm);
-  \node[white] at (2,1) {\small tainted};
-  \end{scope}}
-
-  \only&lt;5-&gt;{
-  \begin{scope}
-  \draw [clip] (0,0) circle (2.955cm);
-  \draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm);
-  \node[white] at (2,1) {\small tainted};
-  \end{scope}}
+  \begin{itemize}
+  \item our proof-technique is adapted from security 
+  protocols\bigskip
+ 
+  \item do not venture outside your field of expertise 
+  \includegraphics[scale=0.03]{smiley.jpg}
+  \bigskip
 
-  \only&lt;6-&gt;{
-  \draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm);
-  \draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm);
-  \node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};
-  }
-
-  \end{tikzpicture}
-  \end{center}
-  
-  \only&lt;7-&gt;{
-  \begin{textblock}{4}(1,12)
-  \small
-  reduced the problem to a finite problem; gave a proof
-  \end{textblock}} 
+  \item we solved the single-processor case; the multi-processor 
+  case: no idea!
+  \end{itemize}
 
   \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Regular Expressions}
+
+
+\begin{textblock}{6}(2,5)
+  \begin{tabular}{rrl@ {\hspace{13mm}}l}
+  \bl{$r$} &amp; \bl{$::=$}  &amp; \bl{$\varnothing$}   &amp; null\\
+           &amp; \bl{$\mid$} &amp; \bl{$\epsilon$}      &amp; empty string\\
+           &amp; \bl{$\mid$} &amp; \bl{$c$}             &amp; character\\
+           &amp; \bl{$\mid$} &amp; \bl{$r_1 \cdot r_2$} &amp; sequence\\
+           &amp; \bl{$\mid$} &amp; \bl{$r_1 + r_2$}     &amp; alternative / choice\\
+           &amp; \bl{$\mid$} &amp; \bl{$r^*$}           &amp; star (zero or more)\\
+  \end{tabular}
+  \end{textblock}
+  
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}
+
+\large
+If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 
+expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
+
+\small
+\bl{$der\,c\,r$} gives the answer, Brzozowski (1964), Owens (2005)
+``\ldots have been lost in the sands of time\ldots''
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{}
+
+
+\ldots{}whether a regular expression can match the empty string:
+\begin{center}
+\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+\bl{$nullable(\varnothing)$}      &amp; \bl{$\dn$} &amp; \bl{$false$}\\
+\bl{$nullable(\epsilon)$}           &amp; \bl{$\dn$} &amp;  \bl{$true$}\\
+\bl{$nullable (c)$}                    &amp; \bl{$\dn$} &amp;  \bl{$false$}\\
+\bl{$nullable (r_1 + r_2)$}       &amp; \bl{$\dn$} &amp;  \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
+\bl{$nullable (r_1 \cdot r_2)$} &amp; \bl{$\dn$} &amp;  \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
+\bl{$nullable (r^*)$}                 &amp; \bl{$\dn$} &amp; \bl{$true$} \\
+\end{tabular}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}
+
+\begin{center}
+\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+  \bl{$der\, c\, (\varnothing)$}      &amp; \bl{$\dn$} &amp; \bl{$\varnothing$} &amp; \\
+  \bl{$der\, c\, (\epsilon)$}           &amp; \bl{$\dn$} &amp; \bl{$\varnothing$} &amp; \\
+  \bl{$der\, c\, (d)$}                     &amp; \bl{$\dn$} &amp; \bl{if $c = d$ then $\epsilon$ else $\varnothing$} &amp; \\
+  \bl{$der\, c\, (r_1 + r_2)$}        &amp; \bl{$\dn$} &amp; \bl{$der\, c\, r_1 + der\, c\, r_2$} &amp; \\
+  \bl{$der\, c\, (r_1 \cdot r_2)$}  &amp; \bl{$\dn$}  &amp; \bl{if $nullable (r_1)$}\\
+  &amp; &amp; \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 
+  &amp; &amp; \bl{else $(der\, c\, r_1) \cdot r_2$}\\
+  \bl{$der\, c\, (r^*)$}          &amp; \bl{$\dn$} &amp; \bl{$(der\,c\,r) \cdot (r^*)$} &amp;\medskip\\\pause
+
+  \bl{$\textit{ders}\, []\, r$}     &amp; \bl{$\dn$} &amp; \bl{$r$} &amp; \\
+  \bl{$\textit{ders}\, (c\!::\!s)\, r$} &amp; \bl{$\dn$} &amp; \bl{$\textit{ders}\,s\,(der\,c\,r)$} &amp; \\
+  \end{tabular}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}\bl{$({\tt a}?)^n \cdot {\tt a}^n$}\end{tabular}}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+\begin{center}
+\begin{tikzpicture}
+\begin{axis}[
+    xlabel={\pcode{a}s},
+    ylabel={time in secs},
+    enlargelimits=false,
+    xtick={0,200,...,1000},
+    xmax=1000,
+    ytick={0,5,...,30},
+    scaled ticks=false,
+    axis lines=left,
+    width=9.5cm,
+    height=7cm, 
+    legend entries={Python,Ruby,Scala V1,Scala V2},  
+    legend pos=north west,
+    legend cell align=left  
+]
+\addplot[blue,mark=*, mark options={fill=white}] 
+  table {re-python.data};
+\addplot[brown,mark=pentagon*, mark options={fill=white}] 
+  table {re-ruby.data};  
+\addplot[red,mark=triangle*,mark options={fill=white}] 
+  table {re1.data};  
+\addplot[green,mark=square*,mark options={fill=white}] 
+  table {re2b.data};
+\end{axis}
+\end{tikzpicture}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{\begin{tabular}{c}\bl{$({\tt a}?)^n \cdot {\tt a}^n$}\end{tabular}}
+
+\begin{center}
+\begin{tikzpicture}
+\begin{axis}[
+    xlabel={\pcode{a}s},
+    ylabel={time in secs},
+    enlargelimits=false,
+    xtick={0,3000,...,12000},
+    xmax=12000,
+    ymax=35,
+    ytick={0,5,...,30},
+    scaled ticks=false,
+    axis lines=left,
+    width=9cm,
+    height=7cm
+]
+\addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};
+\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
+\end{axis}
+\end{tikzpicture}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
-\frametitle{Fuzzy Testing C-Compilers}
+\frametitle{Correctness}
+
+It is a relative easy exercise in a theorem prover:
+
+\begin{center}
+\bl{$matches(r, s)$}  if and only if  \bl{$s \in L(r)$} 
+\end{center}\bigskip
+
+\small
+\bl{$matches(r, s) \dn nullable(ders(r, s))$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{POSIX Regex Matching}
+
+Two rules:
 
 \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:
+\item Longest match rule (``maximal munch rule''): The 
+longest initial substring matched by any regular expression 
+is taken as the next token.
+
+\begin{center}
+\bl{$\texttt{\Grid{iffoo\VS bla}}$}
+\end{center}\medskip
 
-\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}
+\item Rule priority:
+For a particular longest initial substring, the first regular
+expression that can match determines the token.
+
+\begin{center}
+\bl{$\texttt{\Grid{if\VS bla}}$}
+\end{center}
+\end{itemize}\bigskip\pause
+
+\small
+\hfill Kuklewicz: most POSIX matchers are buggy\\
+\footnotesize
+\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}
 
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
-\frametitle{Big Proofs in CS (2)}
+\frametitle{POSIX Regex Matching}
 
 \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}
+
+\item Sulzmann \&amp; Lu came up with a beautiful
+idea for how to extend the simple regular expression 
+matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip\bigskip
+
+\begin{tabular}{@{\hspace{4cm}}c@{}}
+  \includegraphics[scale=0.14]{sulzmann.jpg}\\[-2mm]
+  \hspace{0cm}\footnotesize Martin Sulzmann
+\end{tabular}\bigskip\bigskip
+
+\item the idea: define an inverse operation to the derivatives
 \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, Ironclad Apps, \ldots)\medskip
-\item verified cryptography
-\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}
+\frametitle{Regexes and Values}
+
+Regular expressions and their corresponding values:
+
+\begin{center}
+\begin{columns}
+\begin{column}{3cm}
+\begin{tabular}{@{}rrl@{}}
+  \bl{$r$} &amp; \bl{$::=$}  &amp; \bl{$\varnothing$}\\
+           &amp; \bl{$\mid$} &amp; \bl{$\epsilon$}   \\
+           &amp; \bl{$\mid$} &amp; \bl{$c$}          \\
+           &amp; \bl{$\mid$} &amp; \bl{$r_1 \cdot r_2$}\\
+           &amp; \bl{$\mid$} &amp; \bl{$r_1 + r_2$}   \\
+  \\
+           &amp; \bl{$\mid$} &amp; \bl{$r^*$}         \\
+  \\
+  \end{tabular}
+\end{column}
+\begin{column}{3cm}
+\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
+  \bl{$v$} &amp; \bl{$::=$}  &amp; \\
+           &amp;             &amp; \bl{$Empty$}   \\
+           &amp; \bl{$\mid$} &amp; \bl{$Char(c)$}          \\
+           &amp; \bl{$\mid$} &amp; \bl{$Seq(v_1,v_2)$}\\
+           &amp; \bl{$\mid$} &amp; \bl{$Left(v)$}   \\
+           &amp; \bl{$\mid$} &amp; \bl{$Right(v)$}  \\
+           &amp; \bl{$\mid$} &amp; \bl{$[]$}      \\
+           &amp; \bl{$\mid$} &amp; \bl{$[v_1,\ldots\,v_n]$} \\
+  \end{tabular}
+\end{column}
+\end{columns}
+\end{center}\pause
+
+There is also a notion of a string behind a value: \bl{$|v|$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
-Remember the Bridges example?
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Sulzmann \&amp; Lu Matcher}
+
+We want to match the string \bl{$abc$} using \bl{$r_1$}:
+
+\begin{center}
+\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
+\node (r1)  {\bl{$r_1$}};
+\node (r2) [right=of r1] {\bl{$r_2$}};
+\draw[-&gt;,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause
+\node (r3) [right=of r2] {\bl{$r_3$}};
+\draw[-&gt;,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause
+\node (r4) [right=of r3] {\bl{$r_4$}};
+\draw[-&gt;,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause
+\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$\;\;nullable?$}}};\pause
+\node (v4) [below=of r4] {\bl{$v_4$}};
+\draw[-&gt;,line width=1mm]  (r4) -- (v4);\pause
+\node (v3) [left=of v4] {\bl{$v_3$}};
+\draw[-&gt;,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause
+\node (v2) [left=of v3] {\bl{$v_2$}};
+\draw[-&gt;,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause
+\node (v1) [left=of v2] {\bl{$v_1$}};
+\draw[-&gt;,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause
+\draw[-&gt;,line width=0.5mm]  (r3) -- (v3);
+\draw[-&gt;,line width=0.5mm]  (r2) -- (v2);
+\draw[-&gt;,line width=0.5mm]  (r1) -- (v1);
+\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
+\end{tikzpicture}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t,squeeze]
+\frametitle{Sulzmann \&amp; Lu Paper}
 
 \begin{itemize}
-\item Can we look at our programs and somehow ensure
-they are secure/bug free/correct?\pause\bigskip
+\item I have no doubt the algorithm is correct --- 
+  the problem, I do not believe their proof.
+
+  \begin{center}
+  \begin{bubble}[10cm]\small
+  ``How could I miss this? Well, I was rather careless when 
+  stating this Lemma :)\smallskip
+ 
+  Great example how formal machine checked proofs (and 
+  proof assistants) can help to spot flawed reasoning steps.''
+  \end{bubble}
+  \end{center}\pause
+  
+  \begin{center}
+  \begin{bubble}[10cm]\small
+  ``Well, I don't think there's any flaw. The issue is how to 
+  come up with a mechanical proof. In my world mathematical 
+  proof $=$ mechanical proof doesn't necessarily hold.''
+  \end{bubble}
+  \end{center}\pause
+  
+\end{itemize}
+
+  \only&lt;3&gt;{%
+  \begin{textblock}{11}(1,4.4)
+  \begin{center}
+  \begin{bubble}[10.9cm]\small\centering
+  \includegraphics[scale=0.37]{msbug.png}
+  \end{bubble}
+  \end{center}
+  \end{textblock}}
+  
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}The Proof Idea\\[-1mm] by Sulzmann \&amp; Lu
+\end{tabular}}
+
+\begin{itemize}
+\item introduce an inductively defined ordering relation 
+\bl{$v \succ_r v'$} which captures the idea of POSIX matching
+
+\item the algorithm returns the maximum of all possible
+ values that are possible for a regular expression.\pause
+ \bigskip\small
+ 
+\item the idea is from a paper by Cardelli \&amp; Frisch about 
+greedy matching (greedy $=$ preferring instant gratification to delayed
+repletion):
+
+\item e.g.~given \bl{$(a + (b + ab))^*$} and string \bl{$ab$}
+
+\begin{center}
+\begin{tabular}{ll}
+greedy: &amp; \bl{$[Left(a), Right(Left(b)]$}\\
+POSIX:  &amp; \bl{$[Right(Right(a, b)))]$}  
+\end{tabular}
+\end{center} 
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{}
+\centering
+
+
+\bl{\infer{\vdash Empty : \epsilon}{}}\hspace{15mm}
+\bl{\infer{\vdash Char(c): c}{}}\bigskip
 
-\item Very hard: Anything interesting about programs is equivalent
-to halting problem, which is undecidable.\pause\bigskip
+\bl{\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}}
+\bigskip
+
+\bl{\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}}\hspace{15mm}
+\bl{\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}}\bigskip
+
+\bl{\infer{\vdash [] : r^*}{}}\hspace{15mm}
+\bl{\infer{\vdash [v_1,\ldots, v_n] : r^*}
+          {\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}&lt;1&gt;[c]
+\frametitle{}
+\small
+
+\begin{tabular}{@{}lll@{}}
+\bl{$POSIX(v, r)$} &amp; \bl{$\dn$} &amp; \bl{$\vdash v : r$}\\ 
+ &amp; &amp;   \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v| 
+     \Rightarrow v \succ_{\alert&lt;2&gt;{r}} v')$}
+\end{tabular}\bigskip\bigskip\bigskip
+
+
+\centering
+
+\bl{\infer{Seq(v_1, v_2) \succ_{\alert&lt;2&gt;{r_1\cdot r_2}} Seq(v'_1, v'_2)}
+   {v_1 = v'_1 \quad v_2 \succ_{\alert&lt;2&gt;{r_2}} v'_2}}\hspace{3mm}
+\bl{\infer{Seq(v_1, v_2) \succ_{\alert&lt;2&gt;{r_1\cdot r_2}} Seq(v'_1, v'_2)}
+   {v_1 \not= v'_1 \quad v_1 \succ_{\alert&lt;2&gt;{r_1}} v'_1}}
+\bigskip
+
+\bl{\infer{Left(v) \succ_{\alert&lt;2&gt;{r_1 + r_2}} Left(v')}
+          {v \succ_{\alert&lt;2&gt;{r_1}} v'}}\hspace{15mm}
+\bl{\infer{Right(v) \succ_{\alert&lt;2&gt;{r_1 + r_2}} Right(v')}
+          {v \succ_{\alert&lt;2&gt;{r_2}} v'}}\bigskip\medskip
 
-\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)
+\bl{\infer{Left(v) \succ_{\alert&lt;2&gt;{r_1 + r_2}} Right(v')}
+          {length |v|  \ge length |v'|}}\hspace{15mm}
+\bl{\infer{Right(v) \succ_{\alert&lt;2&gt;{r_1 + r_2}} Left(v')}
+          {length |v| &gt;  length |v'|}}\bigskip
+
+\bl{$\big\ldots$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Problems}
+
+\begin{itemize}
+\item Sulzmann: \ldots Let's assume \bl{$v$} is not 
+    a $POSIX$ value, then there must be another one
+    \ldots contradiction.\bigskip\pause
+
+\item Exists?
+
+\begin{center}
+\bl{$L(r) \not= \varnothing \;\Rightarrow\; POSIX(v, r)$}
+\end{center}\bigskip\bigskip\pause
+
+\item in the sequence case, the induction hypotheses require
+\bl{$|v_1| = |v'_1|$} and \bl{$|v_2| = |v'_2|$}, 
+but you only know
+
+\begin{center}
+\bl{$|v_1| \;@\; |v_2| = |v'_1| \;@\; |v'_2|$}
+\end{center}\pause\small
+
+\item although one begins with the assumption that the two 
+values have the same flattening, this cannot be maintained 
+as one descends into the induction (alternative, sequence)
 \end{itemize}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Our Solution}
+
+\begin{itemize}
+\item direct definition of what a POSIX value is, using
+\bl{$s \in r \to v$}:
+
+\begin{center}
+\bl{\infer{[] \in \epsilon \to Empty}{}}\hspace{15mm}
+\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip
+
+\bl{\infer{s \in r_1 + r_2 \to Left(v)}
+          {s \in r_1 \to v}}\hspace{10mm}
+\bl{\infer{s \in r_1 + r_2 \to Right(v)}
+          {s \in r_2 \to v &amp; s \not\in L(r_1)}}\bigskip\medskip
+
+\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}
+          {\small\begin{array}{l}
+           s_1 \in r_1 \to v_1 \\
+           s_2 \in r_2 \to v_2 \\
+           \neg(\exists s_3\,s_4.\; s_3 \not= []
+           \wedge s_3 @ s_4 = s_2 \wedge
+           s_1 @ s_3 \in L(r_1) \wedge
+           s_4 \in L(r_2))
+           \end{array}}}
+           
+\bl{\ldots}           
+\end{center}
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+  \frametitle{\Large\begin{tabular}{@{}c@{}}Pencil-and-Paper Proofs\\[-1mm] 
+  in CS are normally incorrect\end{tabular}}
+
+\begin{itemize}
+\item case in point, in one of Roy's proofs he made the 
+incorrect inference
+
+\begin{center}
+if \bl{$\forall s.\; |v_2| \alert{\not}\in L(der\,c\,r_1) \cdot s$}
+then \bl{$\forall s.\; c\,|v_2| \alert{\not}\in L(r_1) \cdot s$}
+\end{center}\bigskip
+
+while 
+
+\begin{center}
+if \bl{$\forall s.\; |v_2| \in L(der\,c\,r_1) \cdot s$}
+then \bl{$\forall s.\; c\,|v_2| \in L(r_1) \cdot s$}
+\end{center}
+
+is correct
+
+\end{itemize}
+
+
+\begin{textblock}{11}(12,11)
+\includegraphics[scale=0.15]{roy.jpg}
+\end{textblock}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{Proofs in Math~vs.~in CS}
+  
+  \alert{\bf My theory on why CS-proofs are often buggy}
+  \\[-10mm]\mbox{}
+  
+  \begin{center}
+  \begin{tabular}{@{}cc@{}}
+  \begin{tabular}{@{}p{5.6cm}} 
+  \includegraphics[scale=0.43]{icosahedron.png}\\[2mm] 
+  {\bf Math}: \\
+  \raggedright\small
+  in math, ``objects'' can be ``looked'' at from all 
+  ``angles'';\\\smallskip 
+  non-trivial proofs, but it seems
+  difficult to make mistakes
+  \end{tabular} &amp;
+  \begin{tabular}{p{5cm}} 
+  \includegraphics[scale=0.2]{sel4callgraph.jpg}\\[3mm]
+  \raggedright
+  {\bf Code in CS}: \\
+  \raggedright\small
+  the call-graph of the seL4 microkernel OS;\\\smallskip 
+  easy to make mistakes\\ \mbox{}\\
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Conclusion}
+
+\begin{itemize}
+\item we strengthened the POSIX definition of Sulzmann \&amp; Lu
+  in order to get the inductions through, his proof
+  contained small gaps but had also fundamental flaws\bigskip
+
+\item its a nice exercise for theorem proving
+\item some optimisations need to be aplied to the
+ algorithm in order to become fast enough
+\item can be used for lexing, small little functional 
+ program
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[b]
+  \frametitle{
+  \begin{tabular}{c}
+  \mbox{}\\[13mm]
+  \alert{\Large Thank you very much again}\\
+  \alert{\Large for the invitation!}\\
+  \alert{\Large Questions?}
+  \end{tabular}}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 \end{document}
 




</pre></body></html>