×

Inferring functional properties of matrix manipulating programs by abstract interpretation. (English) Zbl 1425.68074

Summary: We present a new static analysis by abstract interpretation to prove automatically the functional correctness of algorithms implementing matrix operations, such as matrix addition, multiplication, general matrix multiplication, inversion, or more generally 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.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

FunArray; FLAME; ASTREE
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL 1977. ACM, pp 238-252
[2] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proceedings of the PLDI’03. ACM, pp 196-207 · Zbl 1026.68514
[3] Allamigeon X (2008) Non-disjunctive numerical domain for array predicate abstraction. In: SOP 2008, volume 4960 of LNCS. Springer, pp 163-177 · Zbl 1133.68314
[4] Cousot P (2003) Verification by abstract interpretation. In: Verification: theory and practice, essays dedicated to Zohar Manna on the occasion of his 64th birthday, volume 2772 of LNCS. Springer, pp 243-268
[5] Cousot P, Cousot R, Logozzo F (2011) A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of POPL 2011. ACM, pp 105-118 · Zbl 1284.68210
[6] Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceeings of POPL 1978. ACM, pp 84-96
[7] Bondhugula U, Baskaran M, Krishnamoorthy S, Ramanujam J, Rountev A, Sadayappan P (2008) Automatic transformations for communication-minimized parallelization and locality optimization in the polyhedral model. In: CC 2008, volume 4959 of LNCS. Springer, pp 132-146
[8] Bondhugula U, Hartono A, Ramanujam J, Sadayappan P (2008) A practical automatic polyhedral parallelizer and locality optimizer. In: Proceedings of the PLDI 2008. ACM, pp 101-113
[9] Leroy X (2006) Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of the POPL 2006. ACM, pp 42-54 · Zbl 1369.68124
[10] Journault M, Miné A (2016) Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs. In Xavier R (eds) Static analysis—23rd international symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, proceedings, volume 9837 of lecture notes in computer science. Springer, pp 257-277
[11] Venet A (1996) Abstract cofibered domains: application to the alias analysis of untyped programs. In: SAS’96, volume 1145 of LNCS. Springer, pp 366-382
[12] Rival, X.; Mauborgne, L., The trace partitioning abstract domain, ACM Trans. Program. Lang. Syst., 29, 26, (2007)
[13] Cousot P, Cousot R (2002) Modular static program analysis. In: Horspool RN (ed) Compiler construction, 11th international conference, CC 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8-12, 2002, proceedings, volume 2304 of lecture notes in computer science. Springer, pp 159-178 · Zbl 1051.68624
[14] Miné A (2006) Symbolic methods to enhance the precision of numerical abstract domains. In: VMCAI 2006, volume 3855 of LNCS. Springer, pp 348-363 · Zbl 1176.68050
[15] Miné A (2006) The octagon abstract domain. Higher Order Symb Comput (HOSC) 19(1):31-100 http://www-apr.lip6.fr/ mine/publi/article-mine-HOSC06.pdf · Zbl 1105.68069
[16] Gopan D, DiMaio F, Dor N, Reps T, Sagiv M (2004) Numeric domains with summarized dimensions. In: TACAS 2004. Springer, pp 512-529 · Zbl 1126.68348
[17] Gopan D, Reps TW, Sagiv S (2005) A framework for numeric analysis of array operations. In: Proceedings of POPL 2005. ACM, pp 338-350 · Zbl 1369.68138
[18] Halbwachs, N.; Péron, M., Discovering properties about arrays in simple programs, SIGPLAN Not, 43, 339-348, (2008)
[19] Allamigeon X, Godard W, Hymans C (2006) Static analysis of string manipulations in critical embedded C programs. In: SAS 2006. Springer, pp 35-51 · Zbl 1225.68064
[20] Dillig I, Dillig T, Aiken A (2010) Fluid updates: beyond strong vs. weak updates. In: ESOP 2010. Springer, pp 246-266 · Zbl 1260.68092
[21] Monniaux D, Alberti F (2015) A simple abstraction of arrays and maps by program translation. In: SAS 2015, volume 9291 of LNCS. Springer, pp 217-234
[22] Peng Y. Automate convergence rate proof for gradient descent on quadratic functions
[23] Gunnels, JA; Gustavson, FG; Henry, G.; Geijn, RA, FLAME: formal linear algebra methods environment, ACM Trans. Math. Softw., 27, 422-455, (2001) · Zbl 1070.65522
[24] Henzinger TA, Hottelier T, Kovács L, Voronkov A (2010) Invariant and type inference for matrices. In: Barthe G, Hermenegildo MV (eds) Verification, model checking, and abstract interpretation, 11th international conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010, proceedings, volume 5944 of lecture notes in computer science. Springer, pp 163-179
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.