Lit review

2 files changed, 36 insertions, 5 deletions

diff --git a/tex/lit-review/main.tex b/tex/lit-review/main.tex
index 58dc8bb..8f5c5ce 100644
--- a/tex/lit-review/main.tex
+++ b/tex/lit-review/main.tex
@@ -46,7 +46,7 @@ $(+)$, negative $(-)$, zero $(0)$, unknown $(\pm)$ or undefined $(?)$. Using thi
 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
+a "top" $(\top)$ and a "bottom" $(\bot)$ element. The existence of these two
 elements turn our abstract domain into a complete lattice, which ensures some
 helpful properties of our abstract domain.
 
@@ -81,12 +81,44 @@ 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).
+$a_i$ are fixed in advance (a predefined polyhedral shape). This allows for
+ranges to be expressed as $1 \times x_1 + c \ge 0$ provides a single bound for a
+single variable (two such bounds is, of course, a range). Similarly for zones
+one can define a polyhedra $1 \times x_1 + (-1) \times x_2 + c \ge 0$ which is
+equivalent. The octagon domain is $(\pm 1) \times x_1 + (\pm 1) \times x_2 + c
+\ge 0$.
 
 \section{Fixpoints}
-Other test citation: \cite{DBLP:tr/trier/MI96-11}
 
-\section{Strategy Improvement}
+When performing static analysis there is a great need to perform some sort of
+fixpoint solving to determine the possible resultant values for some operations.
+When looping, for instance, it is necessary to "iterate" (in some sense) to find
+what values each variable may take during a loop iteration.
+
+The most basic method for doing so is simply to perform a complete iteration in
+the abstract domain, but doing so has no guarantee of termination and would not
+be expected to be performant. In \cite{CousotCousot77-1} an approach of
+"widening" and "narrowing" is introduced.
+
+This widening/narrowing method performs some fixed number of iteration steps.
+If, after this fixed number, the iteration has not stabilised then it assumes
+that it will not stabilise and will instead continue infinitely, so any affected
+variables are "widened" to infinity. A "narrowing" step is then carried out
+wherein variables are brought back into the finite domain by some terminating
+condition on the loop.
+
+This approach is quite general, and so is applicable to many instances of real
+programs, but is a crude approximation of the reality of the program. In
+specific instances it is possible to perform a better approximation. In
+particular the case of monotonic, expansive operators is considered in \cite{}.  % something from thomas here
+With this approach code points are converted into fixpoint equations with
+$minimum$ and $maximum$ expressions. These fixpoint equations can then be solved
+in order to give information about the program's abstract semantics. These
+equations are solved using the technique of strategy iteration \cite{}  % something about strategy iteration here
+combined with a fast fixpoint-iteration algorithm (such as the one presented in
+\cite{DBLP:tr/trier/MI96-11}).
+
+%Other test citation: \cite{DBLP:tr/trier/MI96-11}
 
 \section{Conclusion}
 
diff --git a/tex/lit-review/references.bib b/tex/lit-review/references.bib
index d3a257b..d6db721 100644
--- a/tex/lit-review/references.bib
+++ b/tex/lit-review/references.bib
@@ -53,7 +53,6 @@
   year      = {2005},
   pages     = {25-41},
   ee        = {http://dx.doi.org/10.1007/978-3-540-30579-8_2},
-  crossref  = {DBLP:conf/vmcai/2005},
   bibsource = {DBLP, http://dblp.uni-trier.de}
 }
 @inproceedings{Dor:2001:CCS:647170.718291,