Dynamic abstract interpretation Patrick Cousot

Abstract interpretation has been used for the design of program semantics, verification and static analysis methods, including typing. We show that abstract interpretation can also be used for dynamic static analysis, at run-time, during program execution, by formalizing all possible instrumented executions and proving their sound relationship with the program semantics.

We take the example of Ramon E. Moore’s interval arithmetics used to put bounds on rounding errors and measurement errors in mathematical computation. Reals are represented by an interval of two floats guaranteed to contain this real. For tests and loops both true and false alternatives may be taken while only one would be taken with reals so that the instrumented semantics must be nondeterministic to be sound and is in general incomplete.