While Abstract Interpreter

Software Verification project developed in the year 2022-2023 by Davide Albiero and Damiano Mason.

The Abstract Interpreter implements 3 types of domains:

• Interval Domain
• Sign Domain
• Congruence Domain

It is also possible to specify the widening delay as a parameter in the constructor of the abstract state.

How it works?

x := 0;

while x < 40 do {
    x++;
};

while x != 0 do {
    x := x - 1;
}

With Interval Domain:

With Sign Domain:

With Congruence Domain:

More examples are available in the Examples folder.