An Abstract Domain Based on Two-Interval Difference-Bound Matrices

In the classical abstract interpretation framework, many abstract domains have some limitations in expressing non-convex properties, which may increase the false alarm rate. Although some abstract domains such as one-variable interval linear inequalities, the powerset of intervals can express non-convex properties, they can not express the relationship between variables. This paper presents a new abstract domain, which is based on Two-Interval Difference-Bound Matrices (tiDBMs). This domain allows us to represent invariants of the form \({x-y\in TI}\), where x and y are variables values and TI is a two-interval such as \([a,b]\cup [c,d]\), where \(a,b,c,d\in \mathbb {R}\).