Deaccumulation techniques for improving provability
Deaccumulation techniques for improving provability
复制标题
用于提高可证明性的去累积技术
DOI：
10.1016/j.jlap.2006.11.001
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
J. Voigtländer
中科院分区：
文献类型：
--
作者：
J. Giesl;Armin Kühnemann;J. Voigtländer
为了机械地验证函数式程序，开发了几个归纳定理证明器。不幸的是，对于具有累积参数的函数，自动验证经常失败。本文利用树传感器理论中的概念，在前人工作的基础上，发展了累加函数程序到非累加函数程序的自动转换，使之更适合于机械化验证。总体目标是减少在(半自动)证明者中推广归纳假设的需要。通过命令式程序与尾递归函数之间的对应关系，该方法还有助于减少命令式程序验证中对循环不变量的需要。
Several induction theorem provers were developed to verify functional programs mechanically. Unfortunately, automatic verification often fails for functions with accumulating arguments. Using concepts from the theory of tree transducers and extending on earlier work, the paper develops automatic transformations from accumulative functional programs into non-accumulative ones, which are much better suited for mechanized verification. The overall goal is to reduce the need for generalizing induction hypotheses in (semi-)automatic provers. Via the correspondence between imperative programs and tail-recursive functions, the presented approach can also help to reduce the need for inventing loop invariants in the verification of imperative programs.