diff options
Diffstat (limited to 'tex/thesis/abstract/abstract.tex')
| -rw-r--r-- | tex/thesis/abstract/abstract.tex | 17 |
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 |