型理論と線形計画法によるマルチスレッドプログラムの安全性検証
【研究分野】ソフトウエア
【研究キーワード】
ソフトウェア検証 / プログラム言語 / 型推論 / 権限計算 / 線形計画法 / 型理論
【研究成果の概要】
本研究は、線形計画法と型理論を応用した、並行ソフトウェアの安全性（例えば、レース状態が起こらないなど）を静的（つまりコンパイル時に)検証する研究である。具体的には「分数権限計算」(FractionalCapability Calculus)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。
【研究代表者】
【研究種目】若手研究(B)
【研究期間】2008 - 2010
【配分額】4,030千円 (直接経費: 3,100千円、間接経費: 930千円)