\documentclass{article}
\usepackage{../style}
\usepackage{../langs}

\begin{document}

\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. 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 few 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, its technical details are too
enormous for explanation here. Therefore let us look at
something much simpler, namely finding out properties about
programs using \emph{static analysis}.

Static analysis is one technique that checks properties
of a program without actually running the program. This
should raise alarm bells---the reason that almost all 
interesting properties about programs are equivalent to
the halting problem, which we know is undecidable. 

\bigskip

\noindent What would be missing in comparison with real
(low-level machine) code? Well, the numbers we assume to be
arbitrary precision, which is not the case in real code. There
basic number formats have a rang and might over-run or
under-run from this range. Our assumption about variables,
does not correspond to actual registers, which are only 
limited on real hardware. Obviously, real code has richer
operations than just addition, multiplication and equality.
But this are not really essential limitations of our simple
examples.

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: