首页    期刊浏览 2024年11月28日 星期四
登录注册

文章基本信息

  • 标题:Certification of Complexity Proofs using CeTA
  • 本地全文:下载
  • 作者:Martin Avanzini ; Christian Sternagel ; Ren{\'e} Thiemann
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:36
  • 页码:23-39
  • DOI:10.4230/LIPIcs.RTA.2015.23
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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.
  • 关键词:complexity analysis; certification; match-bounds; weak dependency pairs; dependency tuples; usable rules; usable replacement maps
国家哲学社会科学文献中心版权所有