sen-material: handouts/ho09.tex@92a718b88e14 (annotated)

276 d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass{article}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	\usepackage{../style}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	\usepackage{../langs}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\begin{document}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
335 06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	7	\section*{Handout 9 (Static Analysis)}
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	8
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	9	If we want to improve the safety and security of our programs,
337 92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	10	we need a more principled approach to programming. Testing is
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	11	good, but as Dijkstra famously said ``Testing can only show
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	12	the presence of bugs, not their absence''. While such a more
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	13	principled approach has been the subject of intense study for
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	14	a long time, only in the past recent years some impressive
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	15	results have been achieved. One is the complete formalisation
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	16	and (mathematical) verification of a microkernel operating
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	17	system called seL4.
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	18
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	19	\begin{center}
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	20	\url{http://sel4.systems}
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	21	\end{center}
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	22
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	23	\noindent In 2011 this work was included in the MIT Technology
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	24	Review in the annual list of the world’s ten most important
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	25	emerging
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	26	technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}}
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	27	While this work is impressive, it technical details are too
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	28	numerous that they can be explained here. So let us look at
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	29	something much simpler, namely finding out properties about
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	30	programs in a very simple programming language using
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	31	\emph{static analysis}.
335 06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	32
276 d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33
335 06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	34	\noindent What would be missing in comparison with real
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	35	(low-level machine) code? Well, the numbers we assume to be
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	36	arbitrary precision, which is not the case in real code. There
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	37	basic number formats have a rang and might over-run or
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	38	under-run from this range. Our assumption about variables,
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	39	does not correspond to actual registers, which are only
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	40	limited on real hardware. Obviously, real code has richer
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	41	operations than just addition, multiplication and equality.
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	42	But this are not really essential limitations of our simple
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	43	examples.
276 d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	\end{document}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	%%% Local Variables:
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	%%% mode: latex
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	%%% TeX-master: t
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Fri, 28 Nov 2014 12:22:50 +0000
changeset 337	92a718b88e14
parent 335	06d5fc15594d
child 338	f1491e0d7be0
permissions	-rw-r--r--