新着情報 テーマカテゴリ 全カテゴリバイオテクノロジー医学・薬学農林水産・食品環境・エネルギー素材機械情報・通信エレクトロニクス航空・宇宙大気・海洋経済・経営・政策・法律土木・建築社会・文化・教育基礎科学 ごあいさつ ご利用にあたり 検索方法 プライバシーポリシー ご意見・ご質問 実例集 見つからない場合は? DUCRホームページへ トップページ geta_logo
print
印刷時に縮小されてしまう場合などにご利用ください。

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


クリックで拡大

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