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

高階関数を用いたプログラム検証および変換技術の高度化に関する研究

Research Project

Project/Area Number 17700002
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionTohoku University

Principal Investigator

青戸 等人  Tohoku University, 電気通信研究所, 准教授 (00293390)

Project Period (FY) 2005 – 2007
Project Status Completed (Fiscal Year 2007)
Budget Amount *help
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2007: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2006: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 2005: ¥700,000 (Direct Cost: ¥700,000)
Keywords項書き換えシステム / 高階関数 / 単純型付き項書き換えシステム / プログラム検証 / 書き換え帰納法 / プログラム変換 / パターン基づくプログラム変換 / 補題自動発見法 / 項群き換えシステム / 帰納的定理証明 / 高階書き換えシステム / 単純型付き書き換えシステム / 変換パターン / 補題自動発見 / 停止性
Research Abstract

単純型付き項書き換えシステムの停止性検証手法の高度化を以下の点について試みた。(1)依存対手法における引数フィルタリングおよび使用可能規則を高階の場合への拡張を行った。(2)実験システムについての検討を進めた。特に、効率的な実装を実現するためのSAT検証器を用いた実装法についての検討を行い、その基本となる経路順序の符号化法について改良を行った。また停止性にもとづく帰納的定理の自動証明法である書き換え帰納法についての検討を進めた。特に反証付き書き換え帰納法に適した補題自動導入法について検討を行った。発散鑑定法を改良し、健全性を持つ発散鑑定法を提案した。実験システムを実装するとともに証明システムのベンチマークとなる例題集を抽出し、他の書き換え帰納法に基づく定理証明器との比較実験を行った。また、反証付き書き換え帰納法を利用するために必要な合流性を保障する方法について検討を進めた。停止性の検証器は多数提案されているのに対して、合流性の検証器の提案はあまりなされていないため、合流性の自動検証法について実験システムを構築し検討を行った。合流性の十分条件を満たさない項書き換えシステムについて分解手法を用いる判定法を利用することの検討を行い、分解手法を利用した合流性検証器の提案を行った。変換パターンに基づくプログラム変換のための変換パターンの抽出法について検討をすすめた。2階の一般化アルゴリズムを提案し、それに基づいて具体的なプログラム変換から変換パターンを抽出する実験を行った。変換に利用可能なパターンの抽出を容易にするためのヒューリスティクスについて検討を行い、いくつかの変換パターンの抽出に成功した。

Report

(3 results)
  • 2007 Annual Research Report
  • 2006 Annual Research Report
  • 2005 Annual Research Report
  • Research Products

    (6 results)

All 2008 2007 2006 2005

All Journal Article (5 results) (of which Peer Reviewed: 3 results) Presentation (1 results)

  • [Journal Article] Automatic Construction of Program Transformation Templates2008

    • Author(s)
      Yuki Chiba, Takahito Aoto, Yoshihito Toyama
    • Journal Title

      IPSJ Transactions on Programming 49

      Pages: 14-27

    • NAID

      130000058178

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Soundness of Rewriting Induction based on an Abstract Principle2008

    • Author(s)
      Takahito Aoto
    • Journal Title

      IPSJ Transactions on Programming 49

      Pages: 28-38

    • NAID

      130000058179

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 項書き換えシステムの合流性自動判定2007

    • Author(s)
      吉田順一, 青戸等人, 外山芳人
    • Journal Title

      情報技術レターズ 6

      Pages: 31-34

    • NAID

      10025982412

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Program Transformation by Template : A Rewriting Framework2006

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

      IPSJ Transactions on Programming 47・SIG16

      Pages: 52-65

    • NAID

      130000058313

    • Related Report
      2006 Annual Research Report
  • [Journal Article] パターンに基づくプログラム変換における列変数の導入2005

    • Author(s)
      千葉勇輝, 青戸等人, 外山芳人
    • Journal Title

      情報技術レターズ 4

      Pages: 5-8

    • Related Report
      2005 Annual Research Report
  • [Presentation] 項書き換えシステム停止性検証器におけるSATソルバ利用のための新しい符号化法2007

    • Author(s)
      青戸等人
    • Organizer
      日本ソフトウェア科学会
    • Place of Presentation
      奈良先端科学技術大学院大学
    • Year and Date
      2007-09-13
    • Related Report
      2007 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi