Inferring functional properties of matrix manipulating programs by abstract interpretation

International audienceWe present a new static analysis by abstract interpretation to prove automatically the functional correctness of algorithms implementing matrix operations , such as matrix addition, multiplication, GEMM (general matrix multiplication), inversion, or more generally BLAS (Basic Linear Algebra Subprograms). In order to do so, we introduce a family of abstract domains parameterized by a set of matrix predicates as well as a numerical domain. We show that our analysis is robust enough to prove the functional correctness of several versions of the same matrix operations, resulting from loop reordering, loop tiling, inverting the iteration order, line swapping, and expression decomposition. We extend our method to enable modular analysis on code fragments manipulating matrices by reference, and show that it results in a significant analysis speedup