From f88d4f700606eb15d83795b188810e0451b2e157 Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Fri, 18 May 2012 13:22:09 +1000 Subject: Add the outline stuff, too. A bit more lit review work. --- tex/outline/main.tex | 68 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 tex/outline/main.tex (limited to 'tex/outline/main.tex') 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} -- cgit v1.2.3