Abstract

CeTA is a tool — whose correctness is formally proven in Isabelle/HOL —
that certifies complexity proofs generated by untrusted complexity analyzers.
We present our recent developments in CeTA that enables certifying exact
complexity bounds for matrix interpretations. We formalized a number of
important results in linear algebra, as well as an implementation of
algebraic numbers.

BibTeX

@inproceedings{JDSJOKRTAY16lcc,
author    = "Jose Divas{\'o}n and Sebastiaan Joosten and
             Ond{\v r}ej Kun{\v c}ar and Ren{\'e} Thiemann and Akihisa Yamada",
title     = "Certifying Exact Complexity Bounds for Matrix Interpretations",
booktitle = "Proceedings of the 16th International Workshop on Logic and
             Computational Complexity",
pages     = {4--7},
year      = 2016
}