\chapter{Introduction}

\section{Motivation}

%Main points:
%  - software is taking on more important roles 
%  - software bugs are dangerous
%  - software bugs are expensive
%  - we have to minimise the number of bugs we have

In today's increasingly technological world, software bugs can have
significant consequences, ranging from the relatively minor
frustration caused to average users to causing deaths. There have been
several incidents in recent years in which a bug in a software system
has led directly to injury or death. X-ray machines which provide too
high a dose of radiation, cars which continue to accelerate against
the driver's wishes and other dangerous situations have all come about
as a direct result of software bugs.

Software bugs also have significant financial costs, with Hailpern and
Santhanam static that debugging, verification and testing can easily
comprise 50\% to 75\% of the total development cost of a
system\cite{Hailpern01softwaredebugging}.

In order to limit the number of bugs we have it has become commonplace
to employ sophisticated approaches to testing. Many different types of
testing are done to attempt to ensure that software is bug-free. These
tests, although extremely useful, are inherently incapable of
\emph{guaranteeing} that software is free of bugs. This is especially
a problem in critical software systems, such as those found in
aeroplanes or large industrial machinery, where software failure can
have catastrophic consequences.

In order to provide a guarantee that software is free of bugs we must
in some way \emph{verify} the software before running it. While it is
possible to write programs in a way that is easier to verify, it is
still a difficult and expensive process to provide verification.

Recently there has been work done in automatically analysing programs
in order to identify bugs. This work is broadly classed \emph{static
  analysis} and this thesis contributes to this work.




\section{Contribution}

In this thesis we present an implementation of the strategy-iteration
based static analyser presented by Gawlitza et
al.\cite{EasyChair:117}. Our implementation has several enhancements
which significantly improve the practical performance of the analyser
on real-world programs.

Theoretical contribution:
\begin{enumerate}
\item
  We present a demand-driven strategy improvement algorithm for
  solving monotonic, expansive equation systems involving $\min$ and
  $\max$ operators
\end{enumerate}

Systems contribution:
\begin{enumerate}
\item
  We develop a solver for monotonic, expansive equation systems based
  on the work of Gawlitza et al.\cite{EasyChair:117} with several
  improvements
\item
  We analyse the performance of our improved solver on a set of
  equation systems to demonstrate the effect of our improvements
\item
  We integrate our solver into the LLVM framework to perform analysis
  over Zones\cite{mine:padoII}
\item
  We analyse the performance of our LLVM analysis on various program inputs
\end{enumerate}