IntervalAI

An abstract interpreter for an integer interval domain supporting basic operations. IntervalAI can verify a C program for correctness against a given specification, provided using assertions. During verification, it treats the domain of each variable as an interval, and performs arithmetic operations, joins, and meets on intervals. It works for a restricted set of C programs consisting only of integer variables.

IntervalAI uses CBMC to convert the C program to a Goto program. It then verifies the Goto program. IntervalAI has been implemented in C++.

Next
Previous