北陸先端科学技術大学院大学 [JAIST] - 研究者総覧
現在ページ トップページ 系別一覧表> 研究者紹介

研究者紹介

研究室
情報研究棟IS Building I 5F
TEL:0761-51-1247
研究室ホームページ
領域ホームページ
 

Japanese

リポジトリ公開資料

共同研究等のお問い合わせは, 産学官連携総合推進センター

 

 

小川 瑞史 (オガワ ミズヒト) 教授
情報科学系、知能ロボティクス領域

■学位

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

■職歴

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

■専門分野

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

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

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

■研究課題

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

■研究業績

◇発表論文

  • A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis,Xin Li, Mizuhito Ogawa,19th International Conference on Formal Engineering Methods,ICFEM17,Springer LNCS
  • raSAT : An SMT Solver for Polynomial Constraints Formal Methods in System Design, Springer,,Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa,Formal Methods in System Design, Springer,Available online,2017/06/27
  • Subtropical Satisfiability,Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Tung Vu,FroCos 2017,Springer LNCS 10483

全件表示

◇講演発表

  • Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract),Masahiko Sakai, Michio Oyamaguchi and Mizuhito Ogawa,IWC 2014 (3rd International Workshop on Confluence,TU Wien, Wien Austria,2014-7-13
  • raSAT: SMT for Polynomial Inequality,To Van Khanh, Vu Xuan Tung and Mizuhito Ogawa,12th International Workshop on Satisfiability Modulo Theories (SMT2014),TU Wien, Wien Austria,2014-7-18

■担当講義

数理論理学,ソフトウェアモデル検査

■学外活動

◇所属学会

  • 情報処理学会 プログラミング研究会,幹事,2007-
  • 情報処理学会 プログラミング研究会,編集委員,2006-
  • 日本ソフトウェア科学会,編集委員,2005-2008

全件表示

◇国際会議主催状況

  • 10th IEEE RIVF International Conference on Computing and Communication Technologies (RIVF-2013),Thanh-Thuy Nguyen・教授(副学長)・VNU-UET, Vietnam、小川瑞史・教授・JAIST, Japan (PC co-chairs),2013-11-10〜13,Hanoi, Vietnam http://uet.vnu.edu.vn/rivf2013/
  • 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013),Hung Dang-Van・教授・UET-VNU Hanoi, Vietnam、小川瑞史・教授・JAIST, Japan (PC co-chairs),2013-10-15〜18,Hanoi, Vietnam http://www.uet.vnu.edu.vn/atva2013/index.htmlProceedings appeared as Springer LNCS 8172

◇審議会等への参画状況

  • 文部科学省大学設置分科会情報専門委員会,大学設置分科会情報専門委員会委員,平成28年10月〜平成29年9月
  • 文部科学省大学設置分科会情報専門委員会 ,大学設置分科会情報専門委員会委員 ,平成27年10月〜平成28年9月
  • 文部科学省大学設置分科会情報専門委員会,大学設置分科会情報専門委員会委員,平成27年4月〜平成27年9月

全件表示