Program verification method based on reduction approximations

基于约简近似的程序验证方法

基本信息

批准号：
14580357
负责人：
TOYAMA Yoshihito
金额：
$ 1.79万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2002
资助国家：
日本
起止时间：
2002 至 2005
项目状态：
已结题

项目摘要

To propose program verification techniques based on reduction approximations, we have studied. rewriting theories among normalization reduction strategies, program transformation by template, termination of higher-order rewriting systems, automated proving for higher-order inductive theorems, decidability of reachability problem. Thorough theoretical analysis and experiments, we have obtained the following results.(1)We proposed the notion of normalizing strategy based on balanced weak confluence. It was shown that external reduction is a normalizing strategy for left-linear term rewriting systems if every critical pair is root balanced joinable. This results expands normalizing strategy of needed reduction. We also presented that external reduction is a computable reduction strategy if regular preserving approximation if it exits.(2)We developed a framework of program transformation by template based on rewriting systems. The correctness of our program transformation method is proven without explicit use of induction on data structures. Thus our program transformation system can easily incorporate with automated theorem provers.(3)We introduce the notion of growing approximation, which is a generalization of strong sequential approximation, NV-sequential approximation and right-linear growing approximation. We have shown that the growing approximation extends the class of term rewriting systems having a decidable normalizing strategy. Moreover, the decidability of confluence and termination for growing systems is presented.

为了根据减少近似提出程序验证技术，我们研究了。重写归一化策略之间的理论，通过模板进行程序转换，高阶重写系统的终止，自动证明高阶归纳定理，可及性问题的可决定性。彻底的理论分析和实验，我们获得了以下结果。（1）我们提出了基于平衡的弱汇合的标准化策略的概念。结果表明，如果每个关键对都是root平衡可加入的，则外部还原是左线术语重写系统的归一化策略。该结果扩大了所需减少的归一化策略。我们还介绍了外部减少是一种可计算的减少策略，如果定期保留近似值，如果它退出。（2）我们基于重写系统开发了模板的程序转换框架。我们的程序转换方法的正确性已被证明，而无需明确使用归纳对数据结构。因此，我们的程序转换系统可以轻松地与自动定理抛弃。（3）我们介绍了增长近似的概念，这是强序近似，NV序列近似和右线增长近似的概括。我们已经表明，增长近似扩展了具有可决定策略的术语重写系统的类别。此外，提出了汇合和终止对生长系统的可决定性。