高階モデル検査によるソフトウェアの全自動検証
カテゴリー
- 情報・通信
SDGs
研究内容
ソフトウェアの信頼性を高めるため、本研究室では、「高階モデル検査」「型理論」などをはじめとする理論計算機科学を駆使してソフトウェアや暗号通信プロトコルを自動検証するための理論およびそれに基づく自動検証ツールの研究を行っている。
現在重点的に取り組んでいる「高階モデル検査」は、ハードウェアやソフトウェアを数学的にモデル化し、網羅的に検証する技術として注目されてきた「モデル検査」をより強力にしたものであり、本研究室において世界に先駆けて実現された検証技術である。本研究室ではこの高階モデル検査手法の改良を進めるとともに、その応用として、プログラムの全自動検証ツールの構築などを行っている。
高階モデル検査に基づく全自動プログラム検証器 MoCHi
© 小林研究室
連携への希望
高階モデル検査手法およびそれに基づくプログラム検証手法を応用し、自社のソフトウェアの品質向上やソフトウェア検証ツールの構築に関心を持つ企業・団体との共同研究を希望する。
公開日 / 更新日
- 2021年12月23日
識別番号
- No. 00182-01