Thesis thesis thesis.

1 files changed, 57 insertions, 8 deletions

diff --git a/tex/thesis/introduction/introduction.tex b/tex/thesis/introduction/introduction.tex
index ffc6cd2..17473af 100644
--- a/tex/thesis/introduction/introduction.tex
+++ b/tex/thesis/introduction/introduction.tex
@@ -36,9 +36,42 @@ 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.
+There has been a continuous stream of research into automatically
+analysing programs in order to identify bugs from the late 70s to the
+present\cite{CousotCousot77-1,EasyChair:117}. This work is broadly
+classed \emph{static analysis} and this thesis contributes to this
+work.
+
+Due to Rice's Theorem\cite{Rice} we know that it is impossible to
+perform a perfect static analysis in general. In order to overcome
+this many approaches to static analysis have been developed, including
+the framework of abstract interpretation presented by Cousot and
+Cousot\cite{CousotCousot77-1}. In this framework we consider a program
+in a simplified, \emph{abstract}, domain. This allows us to perform a
+sound analysis in general at the expense of precision.
+
+Two abstract domains which are particularly well-known and useful are
+those of \emph{interval} and \emph{zones}. The interval abstract
+domain consists of restricting variables in the range $[a,b]$. This
+domain can be useful for avoiding such program errors as division by
+zero errors and out of bounds memory accesses. The abstract domain of
+zones allows us to further place a bound on the difference between
+variables $x - y \le c$. This allows us to be more precise in our
+analysis, thereby avoiding false-positives, at the cost of speed.
+
+The process of determining appropriate bounds for program variables
+has traditionally been performed by performing several Kleene
+iterations, followed by a \emph{widening} and \emph{narrowing}. These
+widening and narrowing operators ensure termination, but once again at
+the cost of precision. As an alternative to these operators we can, in
+some instances, use a game-theoretic approach to compute the abstract
+semantics of a program\cite{EasyChair:117}. This approach is less
+general than widening and narrowing, but performs precise abstract
+interpretation over zones.
+
+In this thesis we present an implementation of this game-theoretic
+algorithm, along with our own enhancements which improve its
+performance on real-world data.
 
 
 
@@ -56,7 +89,7 @@ Theoretical contribution:
 \item
   We present a demand-driven strategy improvement algorithm for
   solving monotonic, expansive equation systems involving $\min$ and
-  $\max$ operators
+  $\max$ operators.
 \end{enumerate}
 
 Systems contribution:
@@ -64,13 +97,29 @@ Systems contribution:
 \item
   We develop a solver for monotonic, expansive equation systems based
   on the work of Gawlitza et al.\cite{EasyChair:117} with several
-  improvements
+  improvements.
 \item
   We analyse the performance of our improved solver on a set of
-  equation systems to demonstrate the effect of our improvements
+  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}
+  over Zones\cite{mine:padoII}.
 \item
-  We analyse the performance of our LLVM analysis on various program inputs
+  We analyse the performance of our LLVM analysis on various program
+  inputs.
 \end{enumerate}
+
+\section{Structure of the thesis}
+
+In Chapter \ref{chap:litreview} we review the background literature in
+the field of static analysis, laying the basis for the rest of the
+thesis. %TODO: more
+
+We present our theoretical contribution in \ref{chap:contribution}: a
+demand-driven strategy improvement algorithm. We present the algorithm
+along with an evaluation of its performance on realistic problems.
+
+Our implementation is discussed in Chapter
+\ref{chap:implementation}. We discuss several aspects of our
+implementation before evaluating the results of our analysis on
+several programs.