summaryrefslogtreecommitdiff
path: root/tex/outline
diff options
context:
space:
mode:
Diffstat (limited to 'tex/outline')
-rw-r--r--tex/outline/Makefile8
-rw-r--r--tex/outline/main.tex68
-rw-r--r--tex/outline/references.bib86
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}
-}