研究課題
本研究は、線形計画法と型理論を応用した、並行ソフトウェアの安全性(例えば、レースが起こらないなど)を検証する研究である。具体的には「分数権限計算」(Fractional Capability Calculus)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。本年度は、以下の成果が得られた。1.多相型による文脈依存な分数権限計算システム従来の分数権限計算は文脈非依存であるため、異なる文脈で同じ関数が呼び出されるプログラムを正確に検証できない場合があった。我々は、parametric polymorphismという多相型の理論を分散権限計算に導入し、文脈依存であり、かつ多項式時間で推論可能なシステムを構築した。2依存型の推論従来の分数権限計算は通常の型システムと同じくプログラムの値に対して非依存なので、例えば、次のようなプログラムをレースがないと正しく検証できない:if(b){x++} || if(b){x++}(P||QはPとQが並列に動くプログラムを表す。)ブール値bに依存する分岐を判別できないためである。これを解決する手段として「依存型」(dependent types)という値に依存する型の概念があるが、自動的に推論するのは困難であった。我々は、モデル検査の研究で広められた、「反例を用いた自動抽象洗練化」(counter example-guided abstraction refinement)の理念に基づいた、自動的に、かつ効率よく依存型を推論する技術を開発した。
すべて 2010 2009
すべて 雑誌論文 (2件) (うち査読あり 2件) 学会発表 (1件)
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL 2010) 45
ページ: 119-130
Proceedings of the 16th International Static Analysis Symposium(SAS 2009) 5673
ページ: 36-51
