License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.23
URN: urn:nbn:de:0030-drops-51875
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5187/
Go to the corresponding LIPIcs Volume Portal

Avanzini, Martin ; Sternagel, Christian ; Thiemann, René

Certification of Complexity Proofs using CeTA

pdf-format:
7.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{avanzini_et_al:LIPIcs:2015:5187,
  author =	{Martin Avanzini and Christian Sternagel and Ren{\'e} Thiemann},
  title =	{{Certification of Complexity Proofs using CeTA}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{23--39},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5187},
  URN =		{urn:nbn:de:0030-drops-51875},
  doi =		{10.4230/LIPIcs.RTA.2015.23},
  annote =	{Keywords: complexity analysis, certification, match-bounds, weak dependency pairs, dependency tuples, usable rules, usable replacement maps}
}

Keywords: complexity analysis, certification, match-bounds, weak dependency pairs, dependency tuples, usable rules, usable replacement maps
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI