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

高階再帰スキームのモデル検査とそのプログラム検証への応用

Research Project

Project/Area Number 10J03842
Research Category

Grant-in-Aid for JSPS Fellows

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

Principal Investigator

塚田 武志  東北大学, 大学院・情報科学研究科, 特別研究員(DC1)

Project Period (FY) 2010 – 2012
Project Status Completed (Fiscal Year 2012)
Budget Amount *help
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2012: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2011: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2010: ¥700,000 (Direct Cost: ¥700,000)
Keywords高階再帰スキーム / 高階モデル検査 / プログラム検証 / ゲーム意味論 / モデル検査 / 型理論
Research Abstract

前年度に引き続いた理論的な側面の研究と、そのプログラム検証への応用について研究を行った。
1.ゲーム意味論と共通型理論の融合
ゲーム意味論と共通型理論は、高階再帰スキームモデル検査問題への2つの主要なアプローチである。
この2つのアプローチの関係を明らかにすることは未解決の課題であったが、我々は2つの結びつける理論(2レベルゲーム意味論)を構築することに成功した。また、この理論を応用することで既知のモデル検査アルゴリズムの計算量の新しい上界など、応用上有用な結果を与えた。
2.ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器
ゲーム意味論に基づいた新しい高階再帰スキームモデル検査器を提案し、その評価を行った。まず、上で与えたゲーム意味論と共通型理論の対応関係を利用して、ゲーム意味論に基づく共通型の推論法を与えた。この推論法は一般には停止するとは限らないものであるが、この手法と抽象実行という技術を組み合わせることで必ず停止するアルゴリズムを得ることができる。高階再帰スキームのモデル検査は共通型の検査・推論に帰着できることが知られているため、得られた共通型推論器はモデル検査器として使うことができる。こうして得られたアルゴリズムが、特定の場合には既存の手法よりも優れていることを、実験的に確かめた。
高階再帰スキームモデル検査はプログラム検証の際のボトルネックであり、この高速化はプログラム検証器の実用化にとって大変重要である。

Report

(3 results)
  • 2012 Annual Research Report
  • 2011 Annual Research Report
  • 2010 Annual Research Report
  • Research Products

    (6 results)

All 2012 2011

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

  • [Journal Article] Two-Level Game Semantics, Intersection Types, and Recursion Schemes2012

    • Author(s)
      C.-H. Luke Ong
    • Journal Title

      Proceedings of ICALP 2012, LNCS

      Volume: 7392 Pages: 325-336

    • DOI

      10.1007/978-3-642-31585-5_31

    • ISBN
      9783642315848, 9783642315855
    • Related Report
      2012 Annual Research Report
    • Peer Reviewed
  • [Journal Article] An Intersection Type System for Deterministic Pushdown Automata2012

    • Author(s)
      Takeshi Tsukada
    • Journal Title

      Proceedings of IFIP-TCS 2012, LNCS

      Volume: 7604 Pages: 357-371

    • DOI

      10.1007/978-3-642-33475-7_25

    • ISBN
      9783642334740, 9783642334757
    • Related Report
      2012 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明2011

    • Author(s)
      塚田武志, 小林直樹
    • Journal Title

      情報処理学会論文誌プログラミング(PRO)

      Volume: 4(2) Pages: 31-47

    • NAID

      110008616675

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Presentation] Two-level game semantics2012

    • Author(s)
      Takeshi Tsukada
    • Organizer
      Games for Logic and Programming Languages VII
    • Place of Presentation
      Dubrovnik, Croatia
    • Year and Date
      2012-06-29
    • Related Report
      2012 Annual Research Report
  • [Presentation] Linear Intersection Types and Game Semantics2011

    • Author(s)
      Takeshi Tsukada
    • Organizer
      Automated Techniques for Higher-Order Program Verification (Shonan Meeting Seminar 005)
    • Place of Presentation
      神奈川県
    • Year and Date
      2011-09-26
    • Related Report
      2011 Annual Research Report
  • [Presentation] 型システムによる高階木変換器の逆像計算2011

    • Author(s)
      塚田武志, 松田一孝
    • Organizer
      第13回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      北海道
    • Year and Date
      2011-03-09
    • Related Report
      2010 Annual Research Report

URL: 

Published: 2010-12-03   Modified: 2024-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi