From ab443f619d207564e4972274c571ef15da70a74c Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro 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