\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}