# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1416886211 0
# Node ID 8eab185fb187b0980908a05cb5609b4428fab43d
# Parent  54a1fbe96b14b1af3b4ba7902a904f69d9854e2d
updated

diff -r 54a1fbe96b14 -r 8eab185fb187 grammar.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/grammar.sty	Tue Nov 25 03:30:11 2014 +0000
@@ -0,0 +1,4 @@
+\usepackage{listproc}
+\usepackage{plstx}
+
+\newcommand*{\meta}[1]{{\ensuremath{\langle}\textit{#1}\/\ensuremath{\rangle}}}
diff -r 54a1fbe96b14 -r 8eab185fb187 slides/slides09.pdf
Binary file slides/slides09.pdf has changed
diff -r 54a1fbe96b14 -r 8eab185fb187 slides/slides09.tex
--- a/slides/slides09.tex	Tue Nov 25 02:04:48 2014 +0000
+++ b/slides/slides09.tex	Tue Nov 25 03:30:11 2014 +0000
@@ -1,7 +1,8 @@
 \documentclass[dvipsnames,14pt,t]{beamer}
 \usepackage{../slides}
+\usepackage{../langs}
 \usepackage{../graphics}
-\usepackage{../langs}
+\usepackage{../grammar}
 
 % beamer stuff 
 \renewcommand{\slidecaption}{APP 09, King's College London}
@@ -701,17 +702,242 @@
   of the initial state, but be less precise about every newly created object.
   \end{itemize}
 
-  \end{frame}}
+  \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
+\begin{frame}[c]
+\frametitle{Big Proofs in CS}
+
+Formal proofs in CS sound like science fiction? Completely irrelevant!
+Lecturer gone mad?\pause
+
+\begin{itemize}
+\item in 2008, verification of a small C-compiler
+\begin{itemize}
+\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
+\item is as good as \texttt{gcc -O1}, but much less buggy 
+\end{itemize}
+\medskip 
+\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
+\begin{itemize}
+\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}
+
+\end{frame}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
-\frametitle{Random Number Generators}
+\frametitle{Goal}
+
+Remember the Bridges example?
+
+\begin{itemize}
+\item Can we look at our programs and somehow ensure
+they are secure/bug free/correct?\pause\bigskip
+
+\item Very hard: Anything interesting about programs is equivalent
+to 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.
+      $\quad\Rightarrow$ static analysis
+\end{itemize}
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{What is Static Analysis?}
+
+  \begin{center}
+  \includegraphics[scale=0.4]{../pics/state.png}
+  \end{center}
+  
+  \begin{itemize}
+  \item depending on some initial input, a program 
+  (behaviour) will ``develop'' over time.
+  \end{itemize}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{What is Static Analysis?}
+
+  \begin{center}
+  \includegraphics[scale=0.4]{../pics/state2.png}
+  \end{center}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{What is Static Analysis?}
+
+  \begin{center}
+  \includegraphics[scale=0.4]{../pics/state3.jpg}
+  \end{center}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{What is Static Analysis?}
+
+  \begin{center}
+  \includegraphics[scale=0.4]{../pics/state4.jpg}
+  \end{center}
+
+  \begin{itemize}
+  \item to be avoided
+  \end{itemize}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{What is Static Analysis?}
+
+  \begin{center}
+  \includegraphics[scale=0.4]{../pics/state5.png}
+  \end{center}
+  
+  \begin{itemize}
+  \item this needs more work
+  \end{itemize}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{What is Static Analysis?}
+
+  \begin{center}
+  \includegraphics[scale=0.4]{../pics/state6.png}
+  \end{center}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[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}
+         | jump? \meta{Exp} \meta{label}
+         | goto \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots\\
+\end{plstx}}
+
+\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}
+         | jump? \meta{Exp} \meta{label}
+         | goto \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots\\
+\end{plstx}}
+
+\begin{textblock}{0}(7.8,2.5)
+\small
+\begin{bubble}[5.6cm]
+\begin{lstlisting}[numbers=none,
+                   basicstyle=\ttfamily,
+                   language={},xleftmargin=3]
+      a := 1
+      n := 5 
+top:  jump? 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}
+         | jump? \meta{Exp} \meta{label}
+         | goto \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots\\
+\end{plstx}}
+
+\begin{textblock}{0}(7.8,3.5)
+\small
+\begin{bubble}[5.6cm]
+\begin{lstlisting}[numbers=none,
+                   basicstyle=\ttfamily,
+                   language={},xleftmargin=3]
+      n := 6
+      m1 := 0
+      m2 := 1
+top:  jump? n = 0 done
+      tmp := m2
+      m2 := m1 + m2
+      m1 := tmp
+      n := n + -1
+      goto top
+done:
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
 \end{document}
 
+%         n := 5 
+% top:    jump? n = 0 done 
+%         a := a * n 
+%         n := n + -1 
+%         goto top 
+% done:
+
+
 %%% Local Variables:  
 %%% mode: latex
 %%% TeX-master: t