Merge branch 'master' of bitbucket.org:czan/honours into HEAD

Conflicts:
	tex/lit-review/main.tex

1 files changed, 64 insertions, 12 deletions

diff --git a/tex/lit-review/main.tex b/tex/lit-review/main.tex
index 1f610f0..58dc8bb 100644
--- a/tex/lit-review/main.tex
+++ b/tex/lit-review/main.tex
@@ -12,24 +12,76 @@
 
 \section{Introduction}
 
-Static analysis is concerned with determining properties of a program's
-semantics without the need to actually execute the program in question.
+Static analysis is concerned with determining as much as possible about a
+program from it without actually running the program. Being able to analyse the
+program statically can provide a wealth of information about the program's
+characteristics without executing it at all.
 
-%Static analysis is concerned with detemining as many of a program's
-%characteristics as is possible without executing the program itself.
-
-%Human error $\rightarrow$ bugs.
-%It'd be nice if we can automatically test for bugs.
-%Static analysis!
+The uses for static analysis vary significantly, from program optimisation
+(eg. constant propagation) to verification of program semantics and bug-finding.
+In critical applications (for example: medial equipment and flight computers)
+static analysis techniques are used to ensure that programs are free from errors
+which would cause catastrophic failure.
 
+Of particular use in static analysis is the determination of integral values
+within a program. By determining which possible values any integer variables in
+the program can take at each code point it is possible to detect a significant
+number of errors relating to improper integral values (divide-by-zero,
+array-out-of-bounds, etc.). Such errors are among the most common in real-world
+software development, so their detection is of much use to software developers.
 
 \section{Abstract Interpretation}
-Came from: \cite{CousotCousot77-1}.
+
 \subsection{General Framework}
-More in detail about \cite{CousotCousot77-1}.
+
+Abstract interpretation is a technique introduced in \cite{CousotCousot77-1} in
+which a program's semantics are examined within an abstract domain. This
+abstract domain is a simplification of the concrete domain in which the program
+actually executes, but is constructed in such a way as to retain some properties
+of the original program for analysis. We perform our analysis by "executing" our
+program within this abstract domain which we have constructed.
+
+An example of an abstract domain is considering numbers as either positive
+$(+)$, negative $(-)$, zero $(0)$, unknown $(\pm)$ or undefined $(?)$. Using this
+abstraction we can still define some semantics which reflect the program itself
+(as an example: $(+) \times (-) = (-)$, or the product of a positive number with
+a negative number is a negative number). Each abstract domain must also contain
+a "top" $(\top)$ and a "bottom" $(\bottom)$ element. The existence of these two
+elements turn our abstract domain into a complete lattice, which ensures some
+helpful properties of our abstract domain.
+
+By constructing appropriate abstract domains we can infer properties of the
+program's concrete semantics which are relevant to our application. The above
+abstract domain, for example, can be used to detect divide-by-zero errors
+(although it is clear from the above that not all divide-by-zero errors will be
+detected) or negative array-indexing (one form of an out of bounds error).
+
+A number of abstract domains have been conceived and formalised in literature.
+These are considered in the following subsection. An important factor to
+consider in the following is that as abstract domains get more "detailed" they
+become more computationally expensive to analyse.
+
 \subsection{Abstract Domains}
-Difference-bound matrices \cite{mine:padoII}
-Octagon domain \cite{mine:hosc06}
+
+Cousot and Cousot, in \cite{CousotCousot77-1} introduce an abstract domain
+providing an upper and lower bound to each integral value. This domain allows
+them to reason about numbers with greater precision than simply considering
+positive/negative/zero.
+
+The abstract domain of "zones", are handled in \cite{mine:padoII}. These zones
+provide a way to perform analysis on the bounds of variable differences (ie. to
+place bounds as $a - b \leq c$) and are also referred to as Difference Bound
+Matrices (which are used in other model-checking applications
+\cite{Yovine98modelchecking}).
+
+The domain of zones is then extended by the same author into the "Octagon
+Abstract Domain" in \cite{mine:hosc06} which additionally allows bounds on the
+sum of variables ($\pm a \pm b \leq c$).
+
+All of these above domains are actually shown to be instances of the polyhedra
+abstract domain in \cite{DBLP:conf/vmcai/SankaranarayananSM05}. The polyhedra
+domain expresses bounds on $a_1 x_1 + a_2 x_2 ... + a_n x_n + c \ge 0$, where
+$a_i$ are fixed in advance (a predefined polyhedral shape).
 
 \section{Fixpoints}
 Other test citation: \cite{DBLP:tr/trier/MI96-11}