AIInterval checks for program correctness by abstract interpretation in interval domain. It supports C programs comprising of integer variables. It supports 4 basic arithmetic operations: addition, subtraction, multiplication, division. It also implements threshold-based-widening for loops, where the threshold is provided by the user. A program is verified for a specification denoted by assert statements.

The tool is interactive depicting the interpretation process in a step-by-step manner to aid better understanding.

Source