Software verification with interval abstraction

OData support
Hajdu Ákos
Department of Measurement and Information Systems

Software is written by people, who tend to make mistakes. In this era, more and more software code is written. Software code is getting a major part in critical systems as well; such as car controller systems and such system should have to be delivered without computer bugs. More and more technics and methods are invented to test code and detect bugs, and to prove the correctness of the software.

The aim of this thesis is to provide a method to store a set of values that program can take and make calculations on them efficiently with the help of abstraction. For storing values of integers the thesis is going to use interval abstraction, and I also demonstrate how to perform calculations with it. This thesis also provides program execution techniques, and optimizations which combined with abstraction can become a powerful tool for software checking. I also implemented these ideas in a computer program which is also part of the thesis. In the last chapter I am going to make some tests on precision and efficiency of the software.


Please sign in to download the files of this thesis.