blob: 7302dca6fa32095ee0f3a102a3ff1e020c8f337a (
about) (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
\chapter*{Abstract}
In today's increasingly technological world, software bugs can have
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 formal
verification. While it is possible to manually prove software correctness,
it is a difficult and expensive process, usually requiring programs to
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 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
and guaranteeing correctness. We present our own enhancements to
improve the algorithm's running time and evaluate our improvements on
a number of benchmarks.
|
