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

*Corresponding author for this work

Research output: Contribution to journalArticleScientificpeer-review

Abstract

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.

Original languageEnglish
Pages (from-to)177-206
Number of pages30
JournalNumerical algebra, control and optimization
Volume10
Issue number2
DOIs
Publication statusPublished - Jun 2020
MoE publication typeA1 Journal article-refereed

Keywords

  • Matrix iterative algorithms
  • Schulz algorithm
  • Reachability analysis
  • Formal verification
  • HYBRID SYSTEMS
  • COVERAGE

Fingerprint

Dive into the research topics of 'FORMAL ANALYSIS OF THE SCHULZ MATRIX INVERSION ALGORITHM: A PARADIGM TOWARDS COMPUTER AIDED VERIFICATION OF GENERAL MATRIX FLOW SOLVERS'. Together they form a unique fingerprint.

Cite this