\documentclass[dvipsnames,14pt,t]{beamer}

\usepackage{slides}

\usepackage{langs}

\usepackage{graph}

\usepackage{soul}

\usepackage{data}

\usepackage{proof}

% beamer stuff 

\renewcommand{\slidecaption}{SMAL, 23.3.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 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}{c}

  \small Christian Urban\\

  %\small King's College London\\

  \\

  \small joint work with Fahad Ausaf and Roy Dyckhoff

  \end{tabular}

  \end{center}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Why Bother?}

\begin{itemize}

\item Surely regular expressions must have been studied and

      implemented to death by now, no?\medskip\pause

\item \ldots{}well, take for example the ``evil'' regular

      expression \bl{$({\tt a}^?)^n \cdot {\tt a}^n$} to match

      strings \bl{$\underbrace{{\tt a}\ldots{\tt a}}_n$}

\end{itemize}\smallskip

\begin{center}

\begin{tikzpicture}

\begin{axis}[

    xlabel={strings of {\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=7cm,

    height=5cm, 

    legend entries={Python,Ruby},  

    legend pos=north west,

    legend cell align=left  

]

\addplot[blue,mark=*, mark options={fill=white}] 

  table {data/re-python.data};

\addplot[brown,mark=pentagon*, mark options={fill=white}] 

  table {data/re-ruby.data};  

\end{axis}

\end{tikzpicture}

\end{center}

\end{frame}

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

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

  \begin{frame}[c]

  \begin{center}

  \includegraphics[scale=0.2]{pics/isabelle.png}

  \end{center}

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

  \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 Isabelle Theorem Prover}

\begin{itemize}

\item started to use Isabelle after my PhD (in 2000)

\item the thesis included a rather complicated

      ``pencil-and-paper'' proof for a termination argument

      (SN for a 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]{pics/barendregt.jpg}\\[-2mm]

  \footnotesize Henk Barendregt

  \end{tabular}

  \hspace{2mm}

  \begin{tabular}{@ {}c@ {}}

  \includegraphics[scale=0.20]{pics/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}[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<2->{

\begin{textblock}{3}(13,5)

\includegraphics[scale=0.33]{pics/skeleton.jpg}

\end{textblock}}

\begin{textblock}{3}(5.3,7)

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

\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 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]{pics/harper.jpg}\\[-2mm]

{\footnotesize Bob Harper}\\[-2mm]

{\footnotesize}

\end{tabular}

\begin{tabular}{c}

\includegraphics[scale=0.37]{pics/pfenning.jpg}\\[-2mm]

{\footnotesize Frank Pfenning}\\[-2mm]

{\footnotesize}

\end{tabular} &

\begin{tabular}{p{6cm}}

\raggedright

{published a proof on LF in\\ {\bf ACM Transactions on 

 Computational Logic}, 2005,

$\sim$31pp}

\end{tabular}\\

\\[0mm]

\begin{tabular}{c}

\includegraphics[scale=0.36]{pics/appel.jpg}\\[-2mm] 

{\footnotesize Andrew Appel}\\[-2.5mm]

{\footnotesize}

\end{tabular} &

\begin{tabular}{p{6cm}}

\raggedright

{relied on their proof in a\\ {\bf security} critical application}

\end{tabular}

\end{tabular}

\end{frame}

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

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

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

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

\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}{14}(2,11)

\small

\begin{itemize}

\item<2-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 

803 loc in C including 2 library functions)\\[-3mm]

\item<2-> 167 loc in C implement a type-checker\\ (proved correct by Harper and Pfenning)

\end{itemize}

\end{textblock}

\end{frame}

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

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

  \begin{frame}<2->[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{column}{0.8\textwidth}

  \begin{textblock}{0}(1,2)

  \begin{tikzpicture}

  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

  { \&[-10mm] 

    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

    \node (proof1) [node1] {\large Proof}; \&

    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);

  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}

  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}

  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}

  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

  \onslide<3->{\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<4->{

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

  \begin{bubble}[11cm]

  \small Each time one needs to check $\sim$31pp~of 

  informal paper proofs---impossible without tool support.

  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 by using a theorem prover we were able to keep a large 

  proof consistent with changes in the first definitions\bigskip

  \item it took us appr.~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}

  \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 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, <-, line width = 2mm] (2,-0.1) -- (2, -1);

  }

  \only<5>{

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

   \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, <-, line width = 2mm] (2,-0.1) -- (2, -1);

  }

  \only<7>{

   \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, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);

  }

  \only<8>{

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

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

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

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

   \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 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, <-, line width = 2mm] (2,-0.1) -- (2, -1);

  }

  \only<14>{

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

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

   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);