This paper presents a new numerical abstract domain for static analysis by abstract interpretation. This domain allows us
to represent invariants of the form (
x −
y =
c) and (±
x =
c) , where
x and
y are variables values and
c is an integer or real constant.
Abstract elements are represented by Difference-Bound Matrices, widely used by model-checkers, but we had to design new operators
to meet the needs of abstract interpretation. The result is a complete lattice of infinite height featuring widening, narrowing
and common transfer functions. We focus on giving an efficient O(n
2)re presentation and graph-based O(n
3)algorit hms—where n is the number of variables—and claim that this domain always performs more precisely than the well-known interval domain.
To illustrate the precision/cost tradeoff of this domain, we have implemented simple abstract interpreters for toy imperative
and parallel languages which allowed us to prove some non-trivial algorithms correct.