summaryrefslogtreecommitdiff
path: root/tex/thesis/introduction/introduction.tex
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/introduction/introduction.tex')
-rw-r--r--tex/thesis/introduction/introduction.tex95
1 files changed, 49 insertions, 46 deletions
diff --git a/tex/thesis/introduction/introduction.tex b/tex/thesis/introduction/introduction.tex
index d1b1a39..cf32e3d 100644
--- a/tex/thesis/introduction/introduction.tex
+++ b/tex/thesis/introduction/introduction.tex
@@ -10,45 +10,53 @@
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.
+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}.
+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
+In order to limit the number of bugs in a software system, it has become commonplace
+to employ sophisticated testing approaches. Different testing
+strategies aim to ensure that a software system is bug-free. These
+testing strategies, 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
+aeroplanes or large industrial machinery, where software failures 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.
-
-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 there is no general way
-to statically infer properties of programs. 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.
+In order to provide a guarantee that software is free of bugs we
+employ \emph{software verification}, that analyses software without
+running it. While it is possible to write programs amenable for
+software verification, it is still a difficult and expensive process
+to perform verification on a software system.
+
+There has been a continuous stream of research in
+program analysis for finding bugs starting from the late 70s to the
+present~\cite{CousotCousot77-1,EasyChair:117}. This work is broadly
+categorised as \emph{static program analysis}, and this thesis contributes
+to this research area.
+
+Due to Rice's Theorem~\cite{Rice} we know that it is undecidable to
+statically infer properties of programs. In order to overcome this
+limitation, many approaches to static analysis have been devised
+including the framework of abstract interpretation introduced by
+Cousot and Cousot~\cite{CousotCousot77-1}. To overcome the
+undecidability issues of static program analysis, a program is
+represented in an abstract domain which becomes decidable. A
+connection (also known as homomorphism) between the abstract domain
+and the concrete domain (actual semantics of the program) is
+established. This connection is called a Galois-connection and
+provides a proof framework to show that the static program analysis is
+a ``sound'' approximation of the semantics. The precision of the
+analysis depends on the granularity of the approximation. In general,
+more precise program analyses result in higher complexity classes.
Two abstract domains which are particularly well-known and useful are
those of \emph{interval} and \emph{zones}. The interval abstract
@@ -62,29 +70,23 @@ 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
+widening and narrowing operators ensure termination, but at
+the cost of precision. As an alternative, we employ in this work
+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.
-
-
-
\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
+al.~\cite{EasyChair:117}. Our implementation has several enhancements
which significantly improve the practical performance of the analyser
on real-world programs.
-Theoretical contribution:
+We present one major theoretical contribution:
\begin{enumerate}
\item
We present a demand-driven strategy improvement algorithm for
@@ -92,19 +94,18 @@ Theoretical contribution:
$\max$ operators.
\end{enumerate}
-Systems contribution:
+We present several systems contributions:
\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
+ 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/Clang
- framework\cite{LLVM,LLVM-paper,Clang} to perform analysis over
- Zones\cite{mine:padoII}.
+ framework~\cite{LLVM,LLVM-paper,Clang} to perform analysis over Zones~\cite{mine:padoII}.
\item
We analyse the performance of our LLVM analysis on various program
inputs.
@@ -124,3 +125,5 @@ 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.
+
+We draw our conclusion in \ref{chap:conclusion}.