Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper)

Abstract

Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of An for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations.