From ab443f619d207564e4972274c571ef15da70a74c Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au>
Date: Mon, 26 Nov 2012 20:18:42 +1100
Subject: Thesis thesis thesis.

---
 tex/thesis/abstract/abstract.tex | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'tex/thesis/abstract/abstract.tex')

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
-- 
cgit v1.2.3

