1 files changed, 68 insertions, 0 deletions
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}