\chapter{Introduction}

\section{Motivation}

Software bugs are bad. Bugs have significant costs in terms of time,
money, security and lives. Hailpern and Santhanam state that
debugging, verification and testing can easily range from 50\% to 75\%
of the total development cost of a
system\cite{Hailpern01softwaredebugging}.

\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 data.

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}