We present new abstract domains to prove automatically the functional correctness of algorithms implementing matrix operations, such as matrix addition, multiplication, GEMM (general matrix multi- plication), or more generally BLAS (Basic Linear Algebra Subprograms). In order to do so, we introduce a family of abstract domains parameter- ized by a set of matrix predicates and by a numeric domain. We show that our analysis is robust enough to prove the functional correctness of several versions of matrix addition and multiplication codes result- ing from loop reordering, loop tiling, inverting the iteration order, line swapping, and expression decomposition. Finally, 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.
CITATION STYLE
Journault, M., & Miné, A. (2016). Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9837 LNCS, pp. 257–277). Springer Verlag. https://doi.org/10.1007/978-3-662-53413-7_13
Mendeley helps you to discover research relevant for your work.