# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1417177370 0
# Node ID 92a718b88e14ecc5771abf6b15b86877f5a30b79
# Parent  3cb200fa6d6a78a4edf74a74fe1eff41af2fe3d2
updated

diff -r 3cb200fa6d6a -r 92a718b88e14 handouts/ho09.tex
--- a/handouts/ho09.tex	Thu Nov 27 17:52:17 2014 +0000
+++ b/handouts/ho09.tex	Fri Nov 28 12:22:50 2014 +0000
@@ -7,7 +7,28 @@
 \section*{Handout 9 (Static Analysis)}
 
 If we want to improve the safety and security of our programs,
-we need a more principled approach to programming.
+we need a more principled approach to programming. Testing is
+good, but as Dijkstra famously said ``Testing can only show
+the presence of bugs, not their absence''. While such a more
+principled approach has been the subject of intense study for
+a long time, only in the past recent years some impressive
+results have been achieved. One is the complete formalisation
+and (mathematical) verification of a microkernel operating
+system called seL4.
+
+\begin{center}
+\url{http://sel4.systems}
+\end{center}
+
+\noindent In 2011 this work was included in the MIT Technology
+Review in the annual list of the world’s ten most important
+emerging
+technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}}
+While this work is impressive, it technical details are too
+numerous that they can be explained here. So let us look at
+something much simpler, namely finding out properties about
+programs in a very simple programming language using
+\emph{static analysis}.
 
 
 \noindent What would be missing in comparison with real
diff -r 3cb200fa6d6a -r 92a718b88e14 slides/slides09.pdf
Binary file slides/slides09.pdf has changed
diff -r 3cb200fa6d6a -r 92a718b88e14 slides/slides09.tex
--- a/slides/slides09.tex	Thu Nov 27 17:52:17 2014 +0000
+++ b/slides/slides09.tex	Fri Nov 28 12:22:50 2014 +0000
@@ -3,16 +3,7 @@
 \usepackage{../langs}
 \usepackage{../graphics}
 \usepackage{../grammar}
-
-%\usepackage{soul}
-
-%\newcommand\hl[1]{%
-%    \tikz[baseline,%
-%      outer sep=-15pt, inner sep = 0pt%
-%    ]%
-%   \node[decorate,rectangle,fill=yellow,anchor=text]{#1};%
-%}%
-\newcommand{\hl}[1]{#1}
+\usepackage{soul}
 
 % beamer stuff 
 \renewcommand{\slidecaption}{APP 09, King's College London}
@@ -1140,7 +1131,7 @@
 
 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 are 
+is what the sign of \texttt{a} and \texttt{n} is (they should 
 always positive).
 
 \end{frame}