2002 Fiscal Year Annual Research Report
プログラム解析のための統一型理論の構築・検証とそれに基づく解析器の自動合成
| Project/Area Number |
14702063
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
小林 直樹 東京工業大学, 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Keywords | 型システム / プログラム解析 / 定理証明支援器 / Coq / プログラム抽出 / 構成的プログラミング |
|---|
| Research Abstract |
近年,プログラム解析の最も有望な手法の一つとして型理論に基づく手法が注目されている.本研究では,プログラム解析のための型理論の構築・検証(すなわち解析手法の正しさの証明)を統一的に行うための枠組みを構築し,さらにそれに基づき,構成的プログラミングの考え方を用いて解析器の自動抽出を行う手法の確立を目指している.本年度の研究成果は以下の通り.
1.プログラム解析のための統一的型理論の拡張・改良
種々のプログラム解析を統一的に扱うための型システムとしてこれまで研究してきた,(1)メモリやファイル,ネットワークなど計算機資源へのアクセス方法を統一的に解析するための型システム,(2)並行プログラムにおけるさまざまな通信・同期の整合性を統一的に解析するための型システムの改良を行い,より広い範囲のプログラム解析を扱えるようにした.具体的には,前者については,time regionと呼ぶ新しい概念を導入することにより,Javaバイトコードにおけるオブジェクトの初期化の解析なども統一的に扱えるようになった.
2.型理論に基づくプログラム解析器の抽出実験
正しいプログラム解析器を自動抽出するための実験として,ラムダ計算の(1)単純型システム,および(2)細部をパラメータ化した汎用的型システムを定理証明支援器Coq上で定式化し,Coqのプログラム抽出機能を用いてプログラム解析器(型推論器)の抽出実験を行った.
3.並行計算モデルの定理証明器上での定式化
並行プログラムのための統一的型システムの定式化の前準備として,並行計算モデルであるπ計算の構文および操作的意味,仕様を記述するためのプロセス論理の定式化をCoq上で行った.
|
-
[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)
