FORMAL ANALYSIS OF THE SCHULZ MATRIX INVERSION ALGORITHM: A PARADIGM TOWARDS COMPUTER AIDED VERIFICATION OF GENERAL MATRIX FLOW SOLVERS

Vassilios A. Tsachouridis*, Georgios Giantamidis, Stylianos Basagiannis, Kostas Kouramas

*Tämän työn vastaava kirjoittaja

Tutkimustuotos: LehtiartikkeliArticleScientificvertaisarvioitu

Abstrakti

This paper pilots Schulz generalised matrix inverse algorithm as a paradigm in demonstrating how computer aided reachability analysis and theoretical numerical analysis can be combined effectively in developing verification methodologies and tools for matrix iterative solvers. It is illustrated how algorithmic convergence to computed solutions with required accuracy is mathematically quantified and used within computer aided reachability analysis tools to formally verify convergence over predefined sets of multiple problem data. In addition, some numerical analysis results are used to form computational reliability monitors to escort the algorithm on-line and monitor the numerical performance, accuracy and stability of the entire computational process. For making the paper self-contained, formal verification preliminaries and background on tools and approaches are reported together with the detailed numerical analysis in basic mathematical language. For demonstration purposes, a custom made reachability analysis program based on affine arithmetic is applied to numerical examples.

AlkuperäiskieliEnglanti
Sivut177-206
Sivumäärä30
JulkaisuNumerical algebra, control and optimization
Vuosikerta10
Numero2
DOI - pysyväislinkit
TilaJulkaistu - kesäkuuta 2020
OKM-julkaisutyyppiA1 Julkaistu artikkeli, soviteltu

Sormenjälki

Sukella tutkimusaiheisiin 'FORMAL ANALYSIS OF THE SCHULZ MATRIX INVERSION ALGORITHM: A PARADIGM TOWARDS COMPUTER AIDED VERIFICATION OF GENERAL MATRIX FLOW SOLVERS'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä