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

Conflicts:
	impl/IdSet.hpp
	impl/main.cpp
	impl/systems/long-fixpoint

3 files changed, 162 insertions, 0 deletions

diff --git a/tex/outline/Makefile b/tex/outline/Makefile
new file mode 100644
index 0000000..66eb399
--- /dev/null
+++ b/tex/outline/Makefile
@@ -0,0 +1,8 @@
+all:
+	pdflatex main.tex
+	bibtex main
+	pdflatex main.tex
+	pdflatex main.tex
+
+clean:
+	rm -f *.bbl *.aux *.blg *.log *.pdf *.out
diff --git a/tex/outline/main.tex b/tex/outline/main.tex
new file mode 100644
index 0000000..8c5cf98
--- /dev/null
+++ b/tex/outline/main.tex
@@ -0,0 +1,68 @@
+\documentclass{article}
+
+\usepackage[a4paper]{geometry}
+\usepackage{hyperref}
+\usepackage{amsmath}
+
+\title{INFO5993 \\ Research outline}
+\author{Carlo Zancanaro}
+
+\begin{document}
+\maketitle
+
+\section{Introduction}
+
+As my research contribution I intend to implement an algorithm presented in
+\cite{gawlitza} for solving systems of fixpoint-equations for their least
+solutions. I will then utilise this algorithm for the implementation of a static
+analysis pass, interpreting program semantics over zones, within the LLVM
+compiler framework. Finally I will be evaluating this new technique to determine
+whether it is of practical use in real-world static analysis.
+
+\section{Technologies}
+
+My implementation will be provided in the {\tt C++} programming language, as it
+is the language in which LLVM has been written. It will primarily be designed to
+analyse programs written in the {\tt C} language.
+
+At the conclusion of my thesis I will have an implementation of the above
+algorithm implemented as an LLVM optimisation/analysis pass. This will plug in
+to the LLVM/Clang static-analysis framework in order to leverage the significant
+work that has been done on the LLVM project. This will also mean that I do not
+have to write a complete parser for the {\tt C} programming language (which
+would no doubt be a long and error-prone operation).
+
+\section{Evaluation}
+
+To evaluate the algorithm I will be investigating two factors: execution time
+and analysis range.
+
+\subsection{Execution time}
+
+Given the increased precision of results provided by the above algorithm I will
+be interested in determining the runtime performance of the algorithm. Static
+analysis is traditionally a slow process and so any speed-gains which can be
+made will be especially beneficial to real world applications. This will also
+mean that my optimisations must be especially aggressive to ensure that there is
+no missed opportunity for speed gains to be made.
+
+\subsection{Analysis range}
+
+In the above algorithm there is a trade-off made wherein we sacrifice the
+generality of the algorithm to provide more precise results. An important factor
+in the utility of this algorithm will be whether it is applicable to the
+majority of real-world code. The restrictions in the paper seem to be general
+enough to encompass a large amount of existing code, but it remains to be shown
+empirically whether this is the case.
+
+\section{Conclusion}
+
+My thesis will consist of implementing and evaluating a new approach to
+fixpoint-iteration in order to perform abstract interpretation over zones for
+the verification of program invariants. This implementation will be done within
+the LLVM-compiler framework. The evaluation will particularly consider factors
+of execution time and analysis range of the algorithm.
+
+\bibliographystyle{abbrv}
+\bibliography{references.bib}
+\end{document}
diff --git a/tex/outline/references.bib b/tex/outline/references.bib
new file mode 100644
index 0000000..9735e26
--- /dev/null
+++ b/tex/outline/references.bib
@@ -0,0 +1,86 @@
+@article{DBLP:tr/trier/MI96-11,
+  author    = {Christian Fecht and
+               Helmut Seidl},
+  title     = {An Even Faster Solver for General Systems of Equations},
+  journal   = {Universit{\"a}t Trier, Mathematik/Informatik, Forschungsbericht},
+  volume    = {96-11},
+  year      = {1996},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@inproceedings{CousotCousot77-1,
+  author =    {Cousot, P{.} and Cousot, R{.}},
+  title =     {Abstract interpretation: a unified lattice model for static 
+               analysis of programs by construction or approximation of 
+               fixpoints},
+  pages =     {238--252},
+  booktitle = {Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT 
+               Symposium on Principles of Programming Languages},
+  address =   {Los Angeles, California},
+  publisher = {ACM Press, New York, NY},
+  year =      1977,
+}
+@article{mine:hosc06,
+  author =    {Min\'e, A{.}},
+  title =     {The Octagon Abstract Domain},
+  journal =   {Higher-Order and Symbolic Computation},
+  editor =    {O. Danvy},
+  publisher = {Springer},
+  year =      {2006},
+  volume =    {19},
+  number =    {1},
+  pages =     {31--100},
+  note =      {\url{http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf}}
+}
+@inproceedings{mine:padoII,
+  author    = {Min\'e, A{.}},
+  title     = {A New Numerical Abstract Domain Based on Difference-Bound Matrices},
+  booktitle = {Proc. of the 2d Symp. on Programs as Data Objects (PADO II)},
+  series    = {Lecture Notes in Computer Science},
+  year      = {2001},
+  month     = {May},
+  pages     = {155--172},
+  volume    = {2053},
+  publisher = {Springer},
+  location  = {Aarhus, Danemark},
+  note      = {\url{http://www.di.ens.fr/~mine/publi/article-mine-padoII.pdf}}
+}
+@inproceedings{DBLP:conf/vmcai/SankaranarayananSM05,
+  author    = {Sriram Sankaranarayanan and
+               Henny B. Sipma and
+               Zohar Manna},
+  title     = {Scalable Analysis of Linear Systems Using Mathematical Programming},
+  booktitle = {VMCAI},
+  year      = {2005},
+  pages     = {25-41},
+  ee        = {http://dx.doi.org/10.1007/978-3-540-30579-8_2},
+  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}
+}
+@article{gawlitza,
+  author = {Thomas Martin Gawlitza and Hemut Seidl},
+  title = {Abstract Interpretation over Zones without Widening}
+}