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