• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Program verification method based on reduction approximations

Research Project

Project/Area Number 14580357
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionTohoku 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)
Keywordsreduction 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)
  • 2005 Annual Research Report   Final Research Report Summary
  • 2004 Annual Research Report
  • 2003 Annual Research Report
  • 2002 Annual Research Report
  • Research Products

    (37 results)

All 2006 2005 2004 2002 Other

All Journal Article (24 results) Publications (13 results)

  • [Journal Article] RAPT : A Program Transformation System based on Term Rewriting2006

    • Author(s)
      Yuki Chiba
    • Journal Title

      Proceedings of 8th JSSST Workshop on Programming and Programming Languages

      Pages: 60-74

    • Related Report
      2005 Annual Research Report
  • [Journal Article] 書き換え帰納法における向き付け不能な等式の証明2006

    • Author(s)
      青戸等人
    • Journal Title

      第8回プログラミングおよびプログラミング言語ワークショップ論文集

      Pages: 75-89

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Reduction strategies for left-linear term rewriting systems2005

    • Author(s)
      Yoshihito Toyama
    • Journal Title

      Lecture Notes in Computer Science 3838

      Pages: 198-223

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Introducing sequence variables in program transformation based on templates2005

    • Author(s)
      Yuki Chiba
    • Journal Title

      Information Technology Letters 4

      Pages: 5-8

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Program transformation by templates based on term rewriting2005

    • Author(s)
      Yuki Chiba
    • Journal Title

      Proc. of the 7^th ACM-SIGPLAN International Conference on PPDP

      Pages: 59-69

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Reduction strategies for left-linear term rewriting systems2005

    • Author(s)
      Y.Toyama
    • Journal Title

      Lecture Notes in Computer Science 3838

      Pages: 198-223

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Introducing Sequence Variables in Program Transformation based on Templates2005

    • Author(s)
      Y.Chiba, T.Aoto, Y.Toyama
    • Journal Title

      Information Technology Letters Vol.4

      Pages: 5-8

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Introducing Sequence Variables in Program Transformation based on Templates2005

    • Author(s)
      Yuki Chiba
    • Journal Title

      Information Technology Letters 4

      Pages: 5-8

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Program Transformation by Templates based on Term Rewriting2005

    • Author(s)
      Yuki Chiba
    • Journal Title

      Proceedings of the 7th ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2005)

      Pages: 59-69

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Confluent Term Rewriting Systems2005

    • Author(s)
      Yoshihito Toyama
    • Journal Title

      Lecture Notes in Computer Science 3467

      Pages: 1-1

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Dependency Pairs for Simply Typed Term Rewriting2005

    • Author(s)
      Takahito Aoto
    • Journal Title

      Lecture Notes in Computer Science 3467

      Pages: 120-134

    • Related Report
      2005 Annual Research Report
  • [Journal Article] 修正AC単調意味論経路順序によるAC停止性2005

    • Author(s)
      落合 秀幸
    • Journal Title

      信学技報 COMP2004-76

      Pages: 23-32

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Termination of S-Expression Rewriting Systems2005

    • Author(s)
      Y.Toyama
    • Journal Title

      第6回PPL論文集

      Pages: 17-17

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Termination of S-expression rewriting systems2004

    • Author(s)
      Yoshihito Toyama
    • Journal Title

      Lecture Notes in Computer Science 3091

      Pages: 40-54

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Inductive theorems for higher-order rewriting2004

    • Author(s)
      Takahito Aoto
    • Journal Title

      Lecture Notes in Computer Science 3091

      Pages: 269-284

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Termination of S-Expression Rewriting Systems2004

    • Author(s)
      Y.Toyama
    • Journal Title

      Lecture Notes in Computer Science 3091

      Pages: 40-54

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Inductive Theorems for Higher-Order Rewriting2004

    • Author(s)
      T.Aoto, T.Yamada, Y.Toyama
    • Journal Title

      Lecture Notes in Computer Science 3091

      Pages: 269-284

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Termination of S-Expression Rewriting Systems2004

    • Author(s)
      Y.TOYAMA
    • Journal Title

      Lecture Notes in Comput.Sci. Vol.3091

      Pages: 40-54

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Inductive Theorems for Higher-Order Rewriting2004

    • Author(s)
      T.Aoto
    • Journal Title

      Lecture Notes in Comput.Sci. Vol.3091

      Pages: 269-284

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Termination of simply-typed applicative term rewriting systems2004

    • Author(s)
      T.Aoto
    • Journal Title

      Proceedings of the 2nd International Workshop on HOR

      Pages: 61-65

    • Related Report
      2004 Annual Research Report
  • [Journal Article] 書き換え帰納法に基づくプログラム融合変換2004

    • Author(s)
      坂本邦彦
    • Journal Title

      日本ソフトウェア科学会第21回大会予稿集

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Dccidability for left-linear growing term rewriting systems2002

    • Author(s)
      Takahito Nagaya
    • Journal Title

      Information and Computation 178

      Pages: 499-514

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Decidability for left-linear growing term rewriting systems2002

    • Author(s)
      T.Nagaya, Y.Toyama
    • Journal Title

      Information and Computation Vol.178

      Pages: 499-514

    • NAID

      110000570827

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Journal Article] Program transformation by templates based on term rewriting

    • Author(s)
      Y.Chiba, T.Aoto, Y.Toyama
    • Journal Title

      Proc.of the 7th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming

      Pages: 59-69

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2005 Final Research Report Summary
  • [Publications] T.Aoto: "Termination of simply typed term rewriting systems by translation and labelling"Lecture Notes in Computer Science. Vol.2706. 380-394 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 青戸等人: "単純型付き項書き換え系における停止性の自動証明"情報処理学会論文誌:プログラミング. Vol.44, No.SIG 4. 67-77 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 青戸等人: "高階関数型プログラムにおける帰納的定理証明"情報技術レターズ. Vol.2. 21-22 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 本多洋平: "完備化手続きにおける関数記号の自動導入機構"電気関係学会東北支部連合大会予稿集. 1G-4. 228 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 落合秀幸: "AC-完備化手続きに基づくプログラム融合変換"電気関係学会東北支部連合大会予稿集. 1G-5. 229 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 秋谷 賢司: "優先順位付き書き換えの計算モデル"信学技報. (発表予定). (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] Yohihito Toyama: "Decidability for Left-Linear Growing Term Rewriting Systems"Information and Camputation. 178. 499-514 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Keiichirou Kusakari: "On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique, The First International Workshop on Higher-Order Rewriting"The First International Workshop on Higher-Order Reivriting. HOR'02. 25 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Yoshihito Toyama: "Decidability for Left-Linear Growing Term Rewriting Systems"Information and Camputation. 178. 499-514 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Yoshihito Toyama: "Decision procedure for inductire theorems by rewrting induction"Technical Report of IEICE COMP. 2002-45. 41-45 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 外山 芳人: "書き換え帰納法による帰納的定理の決定手続き"日本ソフトウェア科学会第19回大会論文集. 2002-9. 3A-2 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 鶴川敏孝: "変換パターンに基づく高速プログラム変換"信学技法COMP. 2002-83. 61-68 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 伊藤芳浩: "完備化手続によるプログラム融合変換の停止条件"信学技法COMP. 2002-84. 69-76 (2002)

    • Related Report
      2002 Annual Research Report

URL: 

Published: 2002-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi