DUCR
整理番号 7176   (公開日 2016年09月01日) (カテゴリ 情報・通信)
高階モデル検査によるソフトウェアの全自動検証
●内容  ソフトウェアの信頼性を高めるため、本研究室では、「高階モデル検査」「型理論」などをはじめとする理論計算機科学を駆使してソフトウェアや暗号通信プロトコルを自動検証するための理論およびそれに基づく自動検証ツールの研究を行っている。
 現在重点的に取り組んでいる「高階モデル検査」は、ハードウェアやソフトウェアを数学的にモデル化し、網羅的に検証する技術として注目されてきた「モデル検査」をより強力にしたものであり、本研究室において世界に先駆けて実現された検証技術である。本研究室ではこの高階モデル検査手法の改良を進めるとともに、その応用として、プログラムの全自動検証ツールの構築などを行っている。
   高階モデル検査手法およびそれに基づくプログラム検証手法を応用し、自社のソフトウェアの品質向上やソフトウェア検証ツールの構築に関心を持つ企業・団体との共同研究を希望する。
●研究者
教授 小林 直樹
大学院情報理工学系研究科 コンピュータ科学専攻
●画像



高階モデル検査に基づく全自動プログラム検証器 MoCHi
(C) 小林研究室
mail
上記内容は、各研究者へのインタビューをもとに東京大学 産学連携本部で骨子をまとめたものです。
本件に関する共同研究等のお問い合わせは、左のバナーをクリックしてください。スタッフがお問い合わせをお受けいたします。