summaryrefslogtreecommitdiff
path: root/tex/thesis/introduction
diff options
context:
space:
mode:
authorCarlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au>2012-11-26 20:18:42 +1100
committerCarlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au>2012-11-26 20:18:42 +1100
commitab443f619d207564e4972274c571ef15da70a74c (patch)
tree4d06e93e1f66b3c4e43b1de17557a96a56821823 /tex/thesis/introduction
parent7ad1aed1a3ba88e2c40c82da05b9bf35eedc4096 (diff)
Thesis thesis thesis.
Diffstat (limited to 'tex/thesis/introduction')
-rw-r--r--tex/thesis/introduction/introduction.tex65
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.