blob: 1f6c803c1b43b7a39e01acf6d08fd2cfa1fb7280 (
about) (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\chapter{Conclusion} \label{chap:conclusion}
In this thesis we have presented an enhancement on a game-theoretic
algorithm for efficiently solving systems of monotonic, expansive
equations for their least fixpoints. We implemented this algorithm in
C++ and evaluated its performance relative to the existing approach,
finding it to be significantly faster for practical instances of
equation systems.
We further have integrated our solver into the LLVM/Clang static
analysis framework to perform static analysis of C programs. We
implemented a translation from C programs into monotonic, expansive
equation systems to analyse C programs with abstract interpretation,
in the domain of zones. We have evaluated the results of this analysis
on a number of test cases to evaluate its precision.
\section{Further work}
There are still several areas in which the work of this thesis could
be improved upon:
\begin{itemize}
\item
{\bf Refine variable dependencies} The enhanced DSI algorithm still
over approximates dependencies between variables to a slight
degree. Reducing this over approximation could result in a slight
improvement in the running time of the algorithm.
\item
{\bf Complete the implementation} The provided LLVM/Clang
integration is currently only at a proof-of-concept stage. Only a
subset of the C semantics are currently considered in the analysis
pass. There is significant work to be done to ensure that analysis
can be performed for all, or at least most, C code.
\end{itemize}
|
