A Perron-Frobenius theorem for deciding matrix growth

DOI10.1016/j.jlamp.2021.100699OpenAlexW3177469998MaRDI QIDQ2239274

René Thiemann

Publication date: 3 November 2021

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2021.100699

zbMATH Keywords

complexityspectral radiusIsabelle/HOL

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method

Uses Software

• Isabelle/HOL
• CeTA
• AProVE
• Perron Frobenius
• Archive Formal Proofs
• TcT

Cites Work

• Unnamed Item
• Matrix interpretations for proving termination of term rewriting
• Isabelle/HOL. A proof assistant for higher-order logic
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems
• Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations
• Certification of Termination Proofs Using CeTA
• Termination Competition (termCOMP 2015)
• Automated Complexity Analysis Based on the Dependency Pair Method
• Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
• Verified Real Asymptotics in Isabelle/HOL
• Automated Complexity Analysis Based on Context-Sensitive Rewriting
• Computer Aided Verification
• Modular Complexity Analysis for Term Rewriting

This page was built for publication: A Perron-Frobenius theorem for deciding matrix growth