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

プログラム解析のための統一型理論の構築・検証とそれに基づく解析器の自動合成

Research Project

Project/Area Number14702063
Research Category

Grant-in-Aid for Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionTohoku University(2004)
Tokyo Institute of Technology(2002-2003)

Principal Investigator

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

Project Period (FY) 2002 – 2004
Project Status Completed(Fiscal Year 2004)
Budget Amount *help
¥15,080,000 (Direct Cost : ¥11,600,000、Indirect Cost : ¥3,480,000)
Fiscal Year 2004 : ¥7,020,000 (Direct Cost : ¥5,400,000、Indirect Cost : ¥1,620,000)
Fiscal Year 2003 : ¥5,850,000 (Direct Cost : ¥4,500,000、Indirect Cost : ¥1,350,000)
Fiscal Year 2002 : ¥2,210,000 (Direct Cost : ¥1,700,000、Indirect Cost : ¥510,000)
Keywords型システム / プログラム解析 / 定理証明支援器 / Coq / プログラム抽出 / 構成的プログラミング
Research Abstract

本研究では、プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し、さらにそれに基づき、構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.
1.プログラム解析のための統一型理論の拡張・改良
種々のプログラム解析を統一的に扱うための型システムとして、これまで研究してきた計算機資源使用法解析および並行プログラムの解析を拡張するとともに、並行プログラム解析器TyPiCalを実装し、そのソースプログラムをホームページ上で公開した.
2.型理論に基づくプログラム解析器の抽出実験
正しいプログラム解析器を自動抽出するための実験として、昨年に引き続き、一部をパラメータ化した汎用的型システムライブラリの定理証明支援器Coq上での定式化を行い、その上に単純型付きラムダ計算の定式化を行って汎用ライブラリの有効性を確かめた.昨年度に比べ、準同型写像を使ったライブラリ部分の拡充を行うなどしてライブラリの完成度を高めた.
3.並行プログラムの検証のためのCoq用ライブラリの構築
並行プログラムを定理証明器上で検証するためのCoq用ライブラリの作成を行った.今後は上記1番目の項目の並行プログラムの型に基づく解析の定式化を本ライブラリに組み込んでいく予定である.

Report

(3results)
  • 2004 Annual Research Report
  • 2003 Annual Research Report
  • 2002 Annual Research Report

Research Products

(15results)

All 2005 2004 Other

All Journal Article Publications

  • [Journal Article] Resource Usage Analysis2005

    • Author(s)
      Atsushi Igarashi, Naoki Kobayashi
    • Journal Title

      ACM TOPLAS 27・2(出版予定)

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Verification of Concurrent Programs using the Coq Proof Assistant : a Case Study2005

    • Author(s)
      R.Affeldt, N.Kobayashi, A.Yonezawa
    • Journal Title

      IPSJ Transactions on Programming 46・SIG1

      Pages : 110-120

    • Related Report
      2004 Annual Research Report
  • [Journal Article] A Generic Type System for the Pi-Calculus2004

    • Author(s)
      Atsushi Igarashi, Naoki Kobayashi
    • Journal Title

      Theoretical Computer Science (Elsevier Science Publishers) 311(1-3)

      Pages : 121-163

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type2004

    • Author(s)
      K.Kodama, K.Suenaga, N.Kobayashi
    • Journal Title

      Proceedings of APLAS'04 (Springer LNCS) 3302

      Pages : 41-56

    • Related Report
      2004 Annual Research Report
  • [Journal Article] A Coq Library for Verification of Concurrent Programs2004

    • Author(s)
      Reynald Affeldt, Naoki Kobayashi
    • Journal Title

      Proceedings of LFM 2004

      Pages : 66-83

    • Related Report
      2004 Annual Research Report
  • [Publications] Atsushi Igarashi, Naoki Kobayashi: "Resource Usage Analysis"ACM Transactions on Programming Languages and Systems. (出版予定). (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] Atsushi Igarashi, Naoki Kobayashi: "A Generic Type System for the Pi-Calculus"Theoretical Computer Science. 311・1-3. 121-163 (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security - Theories and Systems, Springer LNCS. 2609. 217-233 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] Naoki Kobayashi: "Useless Code Elimination and Program Slicing for the Pi-Calculus"Proceedings of APLAS'03,Springer LNCS. 2895. 55-72 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] 児玉 紘一, 小林 直樹, 末永 幸平: "順序付き線形型に基づく木構造処理プログラムからストリーム処理プログラムへの変換"PPL2004論文集. 134-149 (2004)

    • Related Report
      2003 Annual Research Report
  • [Publications] Naoki Kobayashi: "A Type System for Lock-Free Processes"Information and Computation. 177. 122-159 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] Naoki Kobayashi: "Time regions and effects for resource usage analysis"Proceedings of ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI'03). 50-61 (2003)

    • Related Report
      2002 Annual Research Report
  • [Publications] F.Iwama, N.Kobayashi: "A New Type system for JVM Lock Primitives"Proceedings of ACM SIGPLAN Workshop on Asia-PEPM'02. 156-168 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security-Theories and Systems, Springer LNCS. (出版予定). (2003)

    • Related Report
      2002 Annual Research Report
  • [Publications] 小林 直樹, 白根 慶太: "低レベル言語のための情報流解析のための型システム"コンピュータソフトウェア. 2(出版予定). (2003)

    • Related Report
      2002 Annual Research Report

URL :

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

Information FAQ News Terms of Use

Powered by NII kakenhi