diff options
Diffstat (limited to 'tex/outline')
| -rw-r--r-- | tex/outline/Makefile | 8 | ||||
| -rw-r--r-- | tex/outline/main.tex | 68 | ||||
| -rw-r--r-- | tex/outline/references.bib | 86 |
3 files changed, 0 insertions, 162 deletions
diff --git a/tex/outline/Makefile b/tex/outline/Makefile deleted file mode 100644 index 66eb399..0000000 --- a/tex/outline/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -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 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} diff --git a/tex/outline/references.bib b/tex/outline/references.bib deleted file mode 100644 index 9735e26..0000000 --- a/tex/outline/references.bib +++ /dev/null @@ -1,86 +0,0 @@ -@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} -} |