Intervallum-based abstract interpretation for verifying invariant properties

OData support
Supervisor:
Dr. Vörös András
Department of Measurement and Information Systems

Software systems are controlling devices that surround us in our everyday life. Many of

these systems are safety-critical (e.g., autonomous vehicles, power plants), thus ensuring

their correct operation is gaining increasing importance. Formal verification techniques

can not only find errors, but can prove the correctness of the software. There are many algorithms

which work for different problems, however complete analysis is often impossible

due to resource constraints (e.g. time) thus some abstraction is needed.

Abstraction-based interpretation is a technique that uses an abstraction domain for the

software and makes the analysis on this domain, which still can provide mathematical

evidence for the correctness of the system. Abstraction only exaggerate the possible states

of a system, if an erroneous state is still not reachable in the abstract version, it was

unreachable in the original as well. However it is possible that we give a false alarm, we

say that the erroneous state is reachable, but in reality it is only reachable because of the

abstraction. Interval abstraction is a type of abstraction, where the abstraction domain

is represented by intervals.

In this work, we implement a library for interval abstraction domain. We do the interpretation

on Control Flow Automata, a formal model for programs. We create a framework

that implements an abstract interpretation using this library. We implement one new

approach using color classes in the interval domain. We also make different algorithms

using various widening tactics. We perform an experiment on a wide range of software

systems including industrial PLC codes. We evaluate the strengths and weaknesses of our

program.

Downloads

Please sign in to download the files of this thesis.