权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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)提出了基于平衡弱合流的归一化策略概念。证明了当每个关键对都是根平衡可接合时，外部约简是左线性项重写系统的一种归一化策略。这一结果扩展了需要还原的正态化策略。在正则保持近似存在的情况下，外部约简是一种可计算的约简策略。(2)开发了基于重写系统的模板程序转换框架。在不显式使用数据结构归纳法的情况下，证明了程序变换方法的正确性。因此，我们的程序转换系统可以很容易地与自动定理证明器相结合。(3)引入了增长逼近的概念，它是对强序列逼近、nv序列逼近和右线性增长逼近的推广。我们已经证明了增长逼近扩展了一类具有可决定规范化策略的项重写系统。此外，还给出了生长系统汇合和终止的可判定性。