Thesis and performance testing related stuff.

1 files changed, 17 insertions, 17 deletions

diff --git a/tex/thesis/abstract/abstract.tex b/tex/thesis/abstract/abstract.tex
index fc10f32..7302dca 100644
--- a/tex/thesis/abstract/abstract.tex
+++ b/tex/thesis/abstract/abstract.tex
@@ -1,26 +1,26 @@
 \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.
+significant consequences. In order to limit the effect of software bugs,
+engineers employ a wide range testing strategies. However, testing
+cannot 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,
+Guaranteeing that software is bug-free requires formal
+verification. While it is possible to manually prove software correctness,
 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.
+be written with annotations amenable for software verification tools. 
+For this process, a high level of skill on the part of the proof writer
+is required as well.
 
-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.
+There has been considerable research interest in devising verification
+techniques for software, but due to Rice's
+Theorem the problem becomes undecidable to prove whether a program
+is correct.
+ 
+By using Abstract Interpretation a sound approximation of the program's
+semantics can be constructed. The approximation reports all bugs but
+may report false positives. In general the precision of the approximation
+depends on the complexity class of the program analysis.  
 
 In this thesis we present an implementation of a game-theoretic static
 analyser described in \cite{EasyChair:117} as a method of finding bugs