diff options
| -rw-r--r-- | tex/lit-review/main.tex | 72 | ||||
| -rw-r--r-- | tex/lit-review/references.bib | 26 |
2 files changed, 89 insertions, 9 deletions
diff --git a/tex/lit-review/main.tex b/tex/lit-review/main.tex index 7135d2c..58dc8bb 100644 --- a/tex/lit-review/main.tex +++ b/tex/lit-review/main.tex @@ -12,22 +12,76 @@ \section{Introduction} -Static analysis is concerned with detemining as many of a program's -characteristics as is possible without executing the program itself. +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. -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} diff --git a/tex/lit-review/references.bib b/tex/lit-review/references.bib index c21a7b8..d3a257b 100644 --- a/tex/lit-review/references.bib +++ b/tex/lit-review/references.bib @@ -56,3 +56,29 @@ crossref = {DBLP:conf/vmcai/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } +@inproceedings{Dor:2001:CCS:647170.718291, + author = {Dor, Nurit and Rodeh, Michael and Sagiv, Shmuel}, + title = {Cleanness Checking of String Manipulations in C Programs via + Integer Analysis}, + booktitle = {Proceedings of the 8th International Symposium on Static + Analysis}, + series = {SAS '01}, + year = {2001}, + isbn = {3-540-42314-1}, + pages = {194--212}, + numpages = {19}, + url = {http://dl.acm.org/citation.cfm?id=647170.718291}, + acmid = {718291}, + publisher = {Springer-Verlag}, + address = {London, UK, UK}, +} +@INPROCEEDINGS{Yovine98modelchecking, + author = {Sergio Yovine}, + title = {Model checking timed automata}, + booktitle = {In European Educational Forum: School on Embedded + Systems}, + year = {1998}, + pages = {114--152}, + publisher = {Springer-Verlag} +} + |