Invertible Linear Transforms of Numerical Abstract Domains

We study systematic changes of numerical domains in abstract interpretation through invertible linear transforms of the Euclidean vector space, namely, through invertible real square matrices. We provide a full generalization, including abstract transfer functions, of the parallelotopes abstract domain, which turns out to be an instantiation of an invertible linear transform to the interval abstraction. Given an invertible square matrix M and a numerical abstraction A, we show that for a linear program P (i.e., using linear assignments and linear tests only), the analysis using the linearly transformed domain M(A) can be obtained by analysing on the original domain A a linearly transformed program \(P^M\). We also investigate completeness of abstract domains for invertible linear transforms. In particular, we show that, perhaps counterintuitively, octagons are not complete for \(45^{\circ }\) rotations and, additionally, cannot be derived as a complete refinement of intervals for some family of invertible linear transforms.