プログラムの効率化および形式的検証


更新:2020/06/16
前の画像
次の画像
特徴・独自性
  • プログラムの効率の改善や形式的検証に関する研究を行っている。短期間で記述したプログラムは実行時間やメモリ使用量について非効率的であることが多いが、この問題に対し、プログラム変換によって機械的に改善する手法の開発に取り組んでいる。また、大規模なプログラムはその複雑さから予期せぬバグを含みやすいが、この問題に対しては、プログラム検証やモデル検査とよばれる数学的手法によって実行前に網羅的に検証する研究も進めている。
実用化イメージ

通常のソフトウェア開発では有限個のテストを通じて動作確認が行われるが、モデル検査器や定理証明支援系などのツールを用いることで、無限個の入力に対して動作が保証されたプログラムの作成を実現できる。

キーワード

研究者

電気通信研究所
計算システム基盤研究部門
コンピューティング情報理論研究室

中野 圭介 教授 
修士(理学)(京都大学)/博士(理学)(京都大学)

Keisuke Nakano, Professor