Mon 8 Jan 2018 09:00 - 10:00 at Museum A - Invited Talk by René Thiemann Chair(s): June Andronick

Matrix interpretations are widely used in automated complexity analysis.
Certifying such analyses boils down to
determining the growth rate of $A^n$ 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.

In this work we formalize
the Perron–Frobenius theorem.
We utilize the theorem to avoid most of the algebraic numbers
needed for certifying complexity analysis,
so that our new algorithm only needs the
rational
arithmetic
when certifying complexity proofs that existing tools can find.
To cover the theorem in its full extent,
we establish a connection between two different Isabelle/HOL
libraries on matrices,
enabling an easy exchange of theorems between both libraries.
This connection crucially relies on the transfer mechanism
in combination with local type definitions, being a non-trivial case study for
these Isabelle tools.

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:00: Invited Talk by René ThiemannCPP at Museum A
Chair(s): June AndronickData61,CSIRO (formerly NICTA) and UNSW
09:00 - 10:00
Talk
CPP
Jose Divasón, Sebastiaan Joosten, Ondřej KunčarTechnische Universität München, Germany, René ThiemannUniversity of Innsbruck, Akihisa Yamada
DOI