\chapter*{Abstract}

In today's increasingly technological world, software bugs can have
significant consequences. In order to limit the effect of these bugs
software engineers employ a wide variety of tests, but these are
insufficient to guarantee that software is bug free.

Guaranteeing that software is bug-free requires some sort of formal
verification. While it is possible to manually prove software correct,
it is a difficult and expensive process, usually requiring programs to
be written in a particular way and requiring a high level of skill on
the part of the proof writer.

There has been considerable research interest in providing a method of
automatically producing these types of proofs, but due to Rice's
Theorem we know it is not possible, in general, to prove the
correctness of programs.

By using Abstract Interpretation we can perform an imprecise analysis
of our program, allowing us to find some, but not all, classes of bugs
in general programs. This imperfect analysis is sufficient to provide
some level of assurance about a program's correctness while still
remaining a practical approach.

In this thesis we present an implementation of a game-theoretic static
analyser described in \cite{EasyChair:117} as a method of finding bugs
and guaranteeing correctness. We present our own enhancements to
improve the algorithm's running time and evaluate our improvements on
a number of benchmarks.