diff options
Diffstat (limited to 'tex/outline/main.tex')
-rw-r--r-- | tex/outline/main.tex | 68 |
1 files changed, 0 insertions, 68 deletions
diff --git a/tex/outline/main.tex b/tex/outline/main.tex deleted file mode 100644 index 8c5cf98..0000000 --- a/tex/outline/main.tex +++ /dev/null @@ -1,68 +0,0 @@ -\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} |