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

• Project/Area Number: 14702063
• Research Category: Grant-in-Aid for Young Scientists (A)
• Allocation Type: Single-year Grants
• Research Field: 計算機科学
• Research Institution: Tohoku University (2004); Tokyo Institute of Technology (2002-2003)
• Principal Investigator: 小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
• Project Period (FY): 2002 – 2004
• Project Status: Completed (Fiscal Year 2004)
• Budget Amount: ¥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番目の項目の並行プログラムの型に基づく解析の定式化を本ライブラリに組み込んでいく予定である.

Research Products

• [Journal Article] Resource Usage Analysis (2005)
  • Author(s): Atsushi Igarashi, Naoki Kobayashi
  • Journal Title: ACM TOPLAS 27・2(出版予定)
• [Journal Article] Verification of Concurrent Programs using the Coq Proof Assistant : a Case Study (2005)
  • Author(s): R.Affeldt, N.Kobayashi, A.Yonezawa
  • Journal Title: IPSJ Transactions on Programming 46・SIG1 Pages: 110-120
  • NAID: 130000022400
• [Journal Article] A Generic Type System for the Pi-Calculus (2004)
  • Author(s): Atsushi Igarashi, Naoki Kobayashi
  • Journal Title: Theoretical Computer Science (Elsevier Science Publishers) 311(1-3) Pages: 121-163
• [Journal Article] Translation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type (2004)
  • Author(s): K.Kodama, K.Suenaga, N.Kobayashi
  • Journal Title: Proceedings of APLAS'04 (Springer LNCS) 3302 Pages: 41-56
• [Journal Article] A Coq Library for Verification of Concurrent Programs (2004)
  • Author(s): Reynald Affeldt, Naoki Kobayashi
  • Journal Title: Proceedings of LFM 2004 Pages: 66-83
• [Publications] Atsushi Igarashi, Naoki Kobayashi: "Resource Usage Analysis"ACM Transactions on Programming Languages and Systems. (出版予定). (2004)
• [Publications] Atsushi Igarashi, Naoki Kobayashi: "A Generic Type System for the Pi-Calculus"Theoretical Computer Science. 311・1-3. 121-163 (2004)
• [Publications] R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security - Theories and Systems, Springer LNCS. 2609. 217-233 (2003)
• [Publications] Naoki Kobayashi: "Useless Code Elimination and Program Slicing for the Pi-Calculus"Proceedings of APLAS'03,Springer LNCS. 2895. 55-72 (2003)
• [Publications] 児玉 紘一, 小林 直樹, 末永 幸平: "順序付き線形型に基づく木構造処理プログラムからストリーム処理プログラムへの変換"PPL2004論文集. 134-149 (2004)
• [Publications] Naoki Kobayashi: "A Type System for Lock-Free Processes"Information and Computation. 177. 122-159 (2002)
• [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)
• [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)
• [Publications] R.Affeldt, N.Kobayashi: "Verification of a Mail Server in Coq"Software Security-Theories and Systems, Springer LNCS. (出版予定). (2003)
• [Publications] 小林 直樹, 白根 慶太: "低レベル言語のための情報流解析のための型システム"コンピュータソフトウェア. 2(出版予定). (2003)