小川　瑞史（オガワ　ミズヒト）　教授
情報科学研究科（情報科学専攻・ソフトウェア科学領域）

■学位

東京大学修士(理学)(1985),東京大学博士(理学)(2002)

■職歴

NTT電気通信研究所・研究員(1985-2001)、科学技術振興事業団・研究員(2002-2003)、北陸先端科学技術大学院大学・特任教授(2003-2007), 北陸先端科学技術大学院大学・教授(2007-), 国立情報学研究所・客員教授(2008-).

■専門分野

形式的検証手法の理論的基礎および応用の研究を進めています。具体的な検証手法は定理証明とモデル検査を中心とし、プログラム解析やセキュリティプロトコル検証への応用を行っています。関連する理論的基礎として、組み合わせ理論に基づく効率的検証アルゴリズム、非線形項書換系、形式言語における決定可能性について研究を進めています。

■研究テーマのキーワード

検証、プログラム解析、定理証明、モデル検査、組み合わせ理論、書換系、形式言語．

■研究課題

大規模Javaプログラムのコンテキスト依存解析
重み付プッシュダウンモデル検査に基づく Java のコンテキスト依存解析を設計・実装する。特に、オブジェクト指向言語におけるコンテキスト依存解析の基本となる Points-to 解析の新たなアルゴリズムを提案し、現在、10000メソッド程度を目標に実装を進めている。実装は前処理として SOOT による中間言語Jimple への変換、ならびにバックエンドとして Weighted PDS ライブラリを用いる。

■研究業績

◇発表論文

SMT for Polynomial Constraints on Real Numbers，To Van Khanh, Mizuhito Ogawa，Electrical Notes on Theoretical COmputer Science, Elsevier / Tools for Automatics Program Analysis (TAPAS 2012)，to appear
A Comparison of Four Association Engines in Divergent Thinking Support Systems on Wikipedia，Kobkrit Viriyayudhakorn, Susumu Kunifuji, and Mizuhito Ogawa，Springer Lecture Notes in Artificial Intelligence /5th International Conference on Knowledge, Information and Creativity Support Systems (KICSS 2010)，6746，226-237
Conditional Weighted Pushdown Systems and Applications，Xin Li, Mizuhito Ogawa，ACM SIGPLAN 2010 Workshop on Partial Evaluation and Program Manipulation (PEPM10)，141-150，2010/01/19

全件表示