Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
type: Item
instance of: scholarly article
title: Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
zbMATH Open document ID: 1458.65035
author: Vassilios A. Tsachouridis
author: Georgios Giantamidis
author: Stylianos Basagiannis
author: Kostas Kouramas
published in: Numerical Algebra, Control and Optimization
publication date: 2020-07-13T00:00:00Z
Mathematics Subject Classification ID: 65F10
Mathematics Subject Classification ID: 15A09
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 7220004
zbMATH Keywords: matrix iterative algorithms
zbMATH Keywords: Schulz algorithm
zbMATH Keywords: reachability analysis
zbMATH Keywords: formal verification
describes a project that uses: LAPACK
describes a project that uses: Breach
describes a project that uses: PyInterval
describes a project that uses: aaflib
describes a project that uses: C2e2
describes a project that uses: KeYmaera
describes a project that uses: Matlab
describes a project that uses: HSolver
describes a project that uses: ACL2
describes a project that uses: RSOLVER
describes a project that uses: SparseMatrix
describes a project that uses: SpaceEx
describes a project that uses: S-TaLiRo
describes a project that uses: d/dt
describes a project that uses: Flow*
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: naco.2019047
OpenAlex ID: W2979344982
cites work: The algorithmic analysis of hybrid systems
cites work: Counterexample-guided predicate abstraction of hybrid systems
cites work: S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems
cites work: Q4806208
cites work: On Iterative Computation of Generalized Inverses and Associated Projections
cites work: Generalized inverses. Theory and applications.
cites work: Hybrid Systems: Computation and Control
cites work: Q4953384
cites work: The inverse, rank and product of tensors
cites work: Computational techniques for hybrid system verification
cites work: Handbook of Model Checking
cites work: A geometrical approach on generalized inverses by Neumann-type series
cites work: Verified Real Number Calculations: A Library for Interval Arithmetic
cites work: Affine arithmetic: concepts and applications
cites work: Flowpipe approximation and clustering in space-time
cites work: Reachability Analysis of Hybrid Systems Using Support Functions
cites work: Q4234084
cites work: Q4503930
cites work: Robust Test Generation and Coverage for Hybrid Systems
cites work: Perturbation theory for matrix equations
cites work: Q4249569
cites work: Q4863999
cites work: A general reliable quadratic form: An extension of affine arithmetic
cites work: Introduction to Interval Analysis
cites work: Test Coverage for Continuous and Hybrid Systems
cites work: Q4000286
cites work: Generalized matrix inversion is not harder than matrix multiplication
cites work: Iterative method for computing the Moore-Penrose inverse based on Penrose equations
cites work: Q4874788
cites work: Hybrid systems: From verification to falsification by combining motion planning and discrete search
cites work: Two finite-time convergent Zhang neural network models for time-varying complex matrix Drazin inverse
cites work: Efficient dynamic error reduction for hybrid systems reachability analysis
cites work: Q3998482
cites work: Q4418863
cites work: Generalized inverses: theory and computations
cites work: Numerical and Symbolic Computations of Generalized Inverses
cites work: Q4342463
cites work: Bounds for eigenvalues using traces
cites work: Randomized algorithms for total least squares problems
Wikidata QID: Q127123744
DOI: 10.3934/NACO.2019047
Recommended article: Computer-Aided Verification for Iterative Matrix Inversion Problems in Systems and Control

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Problem-oriented verification system and its application to linear algebra programs
Similarity Score: 0.8332567
Recommender Run: Recommender Run 3

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs
Similarity Score: 0.8239366
Recommender Run: Recommender Run 3

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Verification of linear algebra programs in the SPEKTR system
Similarity Score: 0.8223217
Recommender Run: Recommender Run 3

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
Similarity Score: 0.81986606
Recommender Run: Recommender Run 3

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Verifying an infinite systolic algorithm using third-order equational methods
Similarity Score: 0.81623435
Recommender Run: Recommender Run 3

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
Similarity Score: 0.81524295
Recommender Run: Recommender Run 3

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Formalization and Execution of Linear Algebra: From Theorems to Algorithms
Similarity Score: 0.81503224
Recommender Run: Recommender Run 3

Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Recommended article)
Recommended article: Formal verification of numerical programs: from C annotated programs to mechanical proofs
Similarity Score: 0.81214917
Recommender Run: Recommender Run 3