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

2009 Fiscal Year Annual Research Report

ソフトウェアの安全性向上のための型理論の深化と応用

Research Project

Project/Area Number 20240001
Research InstitutionTohoku University

Principal Investigator

小林 直樹  Tohoku University, 大学院・情報科学研究科, 教授 (00262155)

Co-Investigator(Kenkyū-buntansha) 五十嵐 淳  京都大学, 大学院・情報学研究科, 准教授 (40323456)
住井 英二郎  東北大学, 大学院・情報科学研究科, 准教授 (00333550)
寺内 多智弘  東北大学, 大学院・情報科学研究科, 助教 (70447150)
Keywordsソフトウェア検証 / 型理論 / モデル検査 / 高階再帰スキーム / 資源使用法解析 / ツリーオートマトン
Research Abstract

本研究では、ソフトウェアの安全性向上のため、ソフトウェアを実行前に検証するための研究を行っている.本年度は、以下の成果が得られた.
1.高階再帰スキームに基づく関数型プログラムの検証手法の拡張
前年度に,関数型プログラムのさまざまな検証問題が高階再帰スキームと呼ばれる無限木を記述するための文法のモデル検査の問題に還元できることを示したが,このプログラム検証方式には,(1)プログラムが単純型システムで型付けされなければならない,(2)整数やリストなどの無限集合上のデータを扱えないという欠点があった.本年度は,リストや木構造処理プログラムの検証を可能にするために,高階木トランスデューサの一種であるHMTPを導入し,その検証問題を高階再帰スキームのモデル検査の問題に還元する手法を考案した.また,これによって、より広範囲の関数型プログラムの検証を行うための道筋が得られた.
2.型理論に基づく高階再帰スキームのモデル検査アルゴリズムの構築と実装
上記1のプログラム検証手法のためには、高階再帰スキームのモデル検査のアルゴリズムが必要であるが,従来知られていたアルゴリズムは極めて効率の悪く,実用には耐えないものだった.それに対し,本研究では典型的な入力に対しては効率よく動作するモデル検査アルゴリズムを考案,実装し,その有効性を示した.
また,高階再帰スキームのモデル検査の計算量について,従来の結果よりも精密な結果を得た.例えば,高階再帰スキームの生成する木が様相μ計算の論理式で表される性質を満たすか否かの判定問題の計算量は,いくつかのパラメタが定数であるという仮定のもとで,高階再帰スキームのサイズに対して多項式時間であることを示した.
3.メモリの使用法の検証のための型理論
C言語のプログラムにおいてfreeとmallocが正しく使われていること(具体的には2重に解放がおきない、mallocされたメモリ領域はプログラム終了時までに解放されるなどの性質)を検査するための検証器を作成し,その有効性を示した.

  • Research Products

    (13 results)

All 2010 2009

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

  • [Journal Article] Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification2010

    • Author(s)
      Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
    • Journal Title

      Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10)

      Pages: 495-508

    • Peer Reviewed
  • [Journal Article] Untyped Recursion Schemes and Infinite Intersection Types2010

    • Author(s)
      Takeshi Tsukada, Naoki Kobayashi
    • Journal Title

      Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'10) 6014

      Pages: 343-357

    • Peer Reviewed
  • [Journal Article] Dependent types from counterexamples2010

    • Author(s)
      Tachio Terauchi
    • Journal Title

      Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL'10) 45

      Pages: 119-130

    • Peer Reviewed
  • [Journal Article] Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus2009

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

      Proceedings of the 36th Internatilonal Collogquium on Automata, Languages and Programming(ICALP'09) 5556(2)

      Pages: 223-234

    • Peer Reviewed
  • [Journal Article] Undecidable Equivalences for Basic Parallel Processes2009

    • Author(s)
      Hans Huttel, Naoki Kobayashi, Takashi Suto
    • Journal Title

      Information and Computation 207(7)

      Pages: 812-819

    • Peer Reviewed
  • [Journal Article] A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes2009

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

      Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science(LICS'09)

      Pages: 179-188

    • Peer Reviewed
  • [Journal Article] Model-Checking Higher-Order Functions2009

    • Author(s)
      Naoki Kobayashi
    • Journal Title

      Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP'09)

      Pages: 25-36

    • Peer Reviewed
  • [Journal Article] Dependent Type Inference with Interpolants2009

    • Author(s)
      Hiroshi Unno, Naoki Kobayashi
    • Journal Title

      Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming(PPDP'09)

      Pages: 277-288

    • Peer Reviewed
  • [Journal Article] A Logical Foundation for Environment Classifiers2009

    • Author(s)
      Takeshi Tsukada, Atsushi Igarashi
    • Journal Title

      Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications(TLCA'09)

      Pages: 341-355

    • Peer Reviewed
  • [Journal Article] A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References2009

    • Author(s)
      Eijiro Sumii
    • Journal Title

      Proceedings of the 18th EACSL Annual Conference on Computer Science Logic(CSL'09) 5771

      Pages: 455-469

    • Peer Reviewed
  • [Journal Article] Polymorphic Fractional Capabilities2009

    • Author(s)
      Hirotoshi Yasuoka, Tachio Terauchi
    • Journal Title

      Proceedings of the 16th International Symposium on Static Analysis(SAS'09) 5673

      Pages: 36-51

    • Peer Reviewed
  • [Presentation] Higher-Order Program Verification and Language-Based Security2009

    • Author(s)
      Naoki Kobayashi
    • Organizer
      13th Annual Asian Computing Science Conference (ASIAN'09)
    • Place of Presentation
      韓国・ソウル
    • Year and Date
      2009-12-16
  • [Presentation] Types and Recursion Schemes for Higher-Order Program Verification2009

    • Author(s)
      Naoki Kobayashi
    • Organizer
      7th Asian Symposium on Programming Languages and Systems (APLAS'09)
    • Place of Presentation
      韓国・ソウル
    • Year and Date
      2009-12-16

URL: 

Published: 2011-06-16   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi