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

• 研究課題/領域番号: 14702063
• 研究種目: 若手研究(A)
• 配分区分: 補助金
• 研究分野: 計算機科学
• 研究機関: 東北大学 (2004); 東京工業大学 (2002-2003)
• 研究代表者: 小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
• 研究期間 (年度): 2002 – 2004
• 研究課題ステータス: 完了 (2004年度)
• 配分額: 15,080千円 (直接経費: 11,600千円、間接経費: 3,480千円); 2004年度: 7,020千円 (直接経費: 5,400千円、間接経費: 1,620千円); 2003年度: 5,850千円 (直接経費: 4,500千円、間接経費: 1,350千円); 2002年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
• キーワード: 型システム / プログラム解析 / 定理証明支援器 / Coq / プログラム抽出 / 構成的プログラミング

研究概要

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

研究成果

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