Thesis thesis thesis.

1 files changed, 17 insertions, 0 deletions

diff --git a/tex/thesis/abstract/abstract.tex b/tex/thesis/abstract/abstract.tex
index 2326f61..fc10f32 100644
--- a/tex/thesis/abstract/abstract.tex
+++ b/tex/thesis/abstract/abstract.tex
@@ -5,6 +5,23 @@ 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