Certification of Complexity Proofs using CeTA

Martin Avanzini 1, 2, * Christian Sternagel 3 René Thiemann 3
* Auteur correspondant
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Nowadays certification is widely employed by automated termination tools for term rewriting, where certifiers support most available techniques. In complexity analysis, the situation is quite different. Although tools support certification in principle, current certifiers implement only the most basic technique, namely, suitably tamed versions of reduction orders. As a consequence, only a small fraction of the proofs generated by state-of-the-art complexity tools can be certified. To improve upon this situation, we formalized a framework for the certification of modular complexity proofs and incorporated it into CeTA. We report on this extension and present the newly supported techniques (match-bounds, weak dependency pairs, dependency tuples, usable rules, and usable replacement maps), resulting in a significant increase in the number of certifiable complexity proofs. During our work we detected conflicts in theoretical results as well as bugs in existing complexity tools.
Type de document :
Communication dans un congrès
26th International Conference on Rewriting Techniques and Applications, Jun 2015, Warsaw, Poland. 〈10.4230/LIPIcs.RTA.2015.23〉
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01252000
Contributeur : Martin Avanzini <>
Soumis le : jeudi 7 janvier 2016 - 10:08:03
Dernière modification le : samedi 27 janvier 2018 - 01:31:37
Document(s) archivé(s) le : vendredi 8 avril 2016 - 13:12:49

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Martin Avanzini, Christian Sternagel, René Thiemann. Certification of Complexity Proofs using CeTA. 26th International Conference on Rewriting Techniques and Applications, Jun 2015, Warsaw, Poland. 〈10.4230/LIPIcs.RTA.2015.23〉. 〈hal-01252000〉

Partager

Métriques

Consultations de la notice

134

Téléchargements de fichiers

73