Program verification method based on reduction approximations
| Project/Area Number |
14580357
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
TOYAMA Yoshihito Tohoku University, Research Institute of Electrical Communication, Professor, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AOTO Takahito Tohoku University, Research Institute of Electrical Communication, Associate Professor, 電気通信研究所, 助教授 (00293390)
KIKUCHI Kentarou Tohoku University, Research Institute of Electrical Communication, Research Associate, 電気通信研究所, 助手 (40396528)
草刈 圭一郎 東北大学, 電気通信研究所, 助手 (90323112)
|
|---|
| Project Period (FY) |
2002 – 2005
|
| Project Status |
Completed (Fiscal Year 2005)
|
| Budget Amount *help |
¥2,800,000 (Direct Cost: ¥2,800,000)
Fiscal Year 2005: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2004: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2003: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2002: ¥500,000 (Direct Cost: ¥500,000)
|
|---|
| Keywords | reduction system / needed reduction / negular preserving approximation / normalizing strategy / external reduction / balanced weak confluence / 変換パターン / 近似木オートマトン / プロトコル検証 / 書き換えシステム / 優先順位付き書き換え / リダクションの近似 / 条件付き書き換え / 構成子システム / リダクションの近以 / 到達可能性 / 停止性 / 逐次性 / 木オートマン |
|---|
| Research Abstract |
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.
|
Report
(5 results)
Research Products
(37 results)
