[English Version]

小林研究室

東京大学 大学院情報理工学系研究科 コンピュータ科学専攻

新着ニュース

研究の概要

本研究室では，ソフトウェアに関する基礎理論とそのプログラム検証などへの応用についての研究を行っています．近年，交通システムや医療機器，電子商取引など世の中の多くのシステムがコンピュータソフトウェアによって制御されており，それらに欠陥があれば大惨事になりかねません．その一方でソフトウェアはますます大規模化・複雑化しており，テスト実行など従来のソフトウェア開発手法では品質の担保が難しくなっています．そこで，数理科学的な手法を用いて機械的にプログラムの検証や変換を行うことによってソフトウェアの信頼性や性能を向上しよう，というのが研究目的です．また，そのような目的を達成するためには，型理論，形式言語とオートマトン，定理証明など，理論計算機科学を深く学び，研究する必要があります．一見理論的興味の対象にしか見えない数学的概念が実は上記のような応用に結び付くことを実感できるのが本研究室で行っている研究の醍醐味でもあります．この研究分野の魅力については こちらもご覧ください

以下，最近の研究テーマの例です．

  1. 高階モデル検査：システム検証技術であるモデル検査の拡張です．最近，世界初の高階モデル検査器の開発に成功して下の2と3のテーマに応用しています．
  2. プログラムの自動検証：上記1の高階モデル検査を利用して，関数型言語MLやオブジェクト指向言語Java用のプログラム自動検証器を作っています．デモページはこちら やこちら
  3. データ圧縮：文字列や木構造データをそれを生成するプログラムの形式で圧縮し，1の高階モデル検査を利用して圧縮したままパターンマッチングなどのデータ操作を行うというテーマです． デモページはこちら
  4. セキュリティプロトコルの自動検証：インターネットショッピングなどで使われる，暗号を用いてパスワードなどの機密情報をやりとりする通信プロトコルの安全性を自動検証する，というテーマです． デモページはこちら

小林研究室を志望される方へ

こちらをご覧ください

メンバー

教職員

学生

OB/OG

（在籍時の身分に記載のない者は，学部生または大学院生、または交換留学生として在籍）

東大小林研（～2000, 2012/4～）OB/OG

東北大旧小林研（2004/10～2012/3）OB/OG

東工大旧小林研（2001～2004/9）OB/OG


〒113-0033
東京都文京区本郷7-3-1
東京大学 大学院情報理工学系研究科 コンピュータ科学専攻
小林研究室