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