[English Version]
小林研究室
東京大学 大学院情報理工学系研究科 コンピュータ科学専攻
新着ニュース
- 中山さんの卒業論文の成果をまとめた論文 Borrowable Fractional Ownership Types for Verification が国際会議 VMCAI 2024 に採択されました。
- 深石さんの修士論文の成果等を基にした論文 Productivity Verification for Functional Programs by Reduction to Termination Verification が国際会議 PEPM 2024 に採択されました。
- 田中さんの卒業論文の成果をまとめた論文 Ownership Types for Verification of Programs with Pointer Arithmetic が国際会議 PEPM 2024 に採択されました。
- 桂さんの修士論文の成果等を基にした論文 Higher-Order Property-Directed Reachability が国際会議 ICFP 2023 に採択されました。
- 服部さんの修士論文の成果等を基にした論文 Gradual Tensor Shape Checking が国際会議 ESOP 2023 に採択されました。
- 棚橋さんの修士論文の成果等を基にした論文 HFLz Validity Checking for Automated Program Verification が国際会議 POPL 2023 に採択されました。
- 向井さんの卒業論文の成果等を基にした論文 Parameterized Recursive Refinement Types for Automated Program Verification が国際会議 SAS 2022 に採択されました。
- 松下さんの修士論文の成果をまとめた論文 RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code が国際会議 PLDI 2022 に採択されました (Distinguished Paper Award 受賞)。
研究の概要
本研究室では，ソフトウェアに関する基礎理論とそのプログラム検証などへの応用についての研究を行っています．近年，交通システムや医療機器，電子商取引など世の中の多くのシステムがコンピュータソフトウェアによって制御されており，それらに欠陥があれば大惨事になりかねません．その一方でソフトウェアはますます大規模化・複雑化しており，テスト実行など従来のソフトウェア開発手法では品質の担保が難しくなっています．そこで，数理科学的な手法を用いて機械的にプログラムの検証や変換を行うことによってソフトウェアの信頼性や性能を向上しよう，というのが研究目的です．また，そのような目的を達成するためには，型理論，形式言語とオートマトン，定理証明など，理論計算機科学を深く学び，研究する必要があります．一見理論的興味の対象にしか見えない数学的概念が実は上記のような応用に結び付くことを実感できるのが本研究室で行っている研究の醍醐味でもあります．この研究分野の魅力については
こちらもご覧ください
以下，最近の研究テーマの例です．
- 高階モデル検査：システム検証技術であるモデル検査の拡張です．最近，世界初の高階モデル検査器の開発に成功して下の2と3のテーマに応用しています．
- プログラムの自動検証：上記1の高階モデル検査を利用して，関数型言語MLやオブジェクト指向言語Java用のプログラム自動検証器を作っています．デモページはこちら
やこちら
- データ圧縮：文字列や木構造データをそれを生成するプログラムの形式で圧縮し，1の高階モデル検査を利用して圧縮したままパターンマッチングなどのデータ操作を行うというテーマです．
デモページはこちら
- セキュリティプロトコルの自動検証：インターネットショッピングなどで使われる，暗号を用いてパスワードなどの機密情報をやりとりする通信プロトコルの安全性を自動検証する，というテーマです．
デモページはこちら
小林研究室を志望される方へ
こちらをご覧ください
メンバー
教職員
- 小林 直樹（教授）
- 酒寄 健（助教）
- Minchao Wu（特任研究員）
- 木村 幸子（秘書）
学生
- 斎藤 新（D3）
- 桂 宏行（D2）
- 佐々木 悠（D2）
- 石川 貴大（D2）
- 田中 泉生（M2）
- 中山 崇（M2）
- 廣部 ゆりか（M2）
- 服部 穣（M2）
- 桂 武蔵（M1）
- 王 隽伟（M1）
OB/OG
（在籍時の身分に記載のない者は，学部生または大学院生、または交換留学生として在籍）
東大小林研（～2000, 2012/4～）OB/OG
- 五十嵐 淳（現職：京都大学 教授）
- 住井 英二郎（現職：東北大学 教授、在籍時：学部4年〜修士課程学生、東北大准教授）
- 松田 一孝（現職：東北大学 准教授、在籍時：助教）
- 海野 広志（現職：筑波大学 准教授、在籍時：博士課程学生（指導委託）および特任研究員）
- 塚田 武志（現職：千葉大学 准教授、在籍時：助教）
- 新屋 良磨（現職：秋田大学 助教、在籍時：特任研究員）
- 浅田 和之（現職：東北大学 助教、在籍時：特任研究員）
- 中村 誠希（現職：東京工業大学 助教、在籍時：特任研究員）
- Adrien Champion（在籍時：特任研究員）
- Christopher Broadbent（在籍時：JSPS 外国人特別研究員、特任研究員）
- 伊藤 宗平（現職：長崎大学 准教授、在籍時：特任研究員）
- Xin Li（在籍時：特任研究員）
- Mahmudul FAISAL Al Ameen（在籍時：特任研究員）
- 佐藤 亮介（現職：東京農工大学 准教授、在籍時：特任講師）
- 松下 祐介
- 浅野 光平
- 深石 廉
- 山田 理紗
- 今井 航一
- 西村 啓佑
- 池田 諒
- 所司 翼
- 向井 遼哉
- 上野 秀斗
- 神戸 隆太
- 棚橋 健人
- 服部 桃子
- Liu Yuxi
- 劉 弘毅
- 潘 宇路
- 本多 健士郎
- 下田 匠
- 仁木 孝行
- 石川 拓真
- 岩山 直樹
- 江口 慎悟
- 押川 広樹
- 三谷 庸
- 郡 茉友子
- 卜部 夏木
- 寺尾 拓
- Tanti Kaveri
- 今井 雄毅
- 鈴木 僚太
- 岡本 伊吹
- 奥山 裕也
- 細井 洋吉
- 中川 知貴
- 諏訪 敬之
- 木戸 肩吾
- 原 将己
- 奥殿 貴仁
- 渡邉 慶一
- 有地 勇太
- Zhengyi Lu
- 永田 雄大
- 千葉 知也
- Anders Kiel Hovgaard
- Chinmay Mahesh Chandak
- 川田 禎彬
- 武田 広太郎
- 安酸 円秀
- 桑原 拓也
- 藤間 幸一
- 松本 雄磨
- 木田 獎太
- 竹井 悠人
- Haruhiko Nakao
- 斎藤 新
- Hideki Kariya
- Akihiro Kihimoto（現職：IBM Research Lab, Dublin）
- 清水 智弘
東北大旧小林研（2004/10～2012/3）OB/OG
- 寺内 多智弘（現職：早稲田大学 教授、在籍時：東北大学助教）
- 末永 幸平
（現職：京都大学 准教授、在籍時：博士課程（東大からの指導委託）および学振PD）
- 西澤 弘毅（現職：神奈川大学 准教授、在籍時：東北大学助教）
- Adrien Piérard
- 佐藤 悠史
- 関根 奏弥
- 飛田 善広
- 丸山 晋矢
- 田渕 直
- 安岡 宏俊
- 伊藤 由貴
- 会田 直浩
- 佐々木 和也
- 髙橋 恵美
- 矢口 和也
- Trevor Adams
- 野中 琳太郎
- 中村 翼
- 中嶋 辰成
- Dian Syahfitra
- 孫 贇徳
- 真鍋 俊之
- 盛 聪
- 若松 健
- 飛澤 健太
- 上野 慎平
- Brian Burg
- 酒井原 理裕
- 佐藤 伸行
- 菊地 大介
- 金子 雄太
- Scatchell Anthony John
- 松野 裕
- 真野 健介
- 岡元 崇紘
- 須藤 尚稔
- 須藤 崇
- 上嶋 祐紀
- 飯村 枝里
- 阿保 純一
- Siivola Jani Petri Mikael
- Randahl Douglas West
- 大坪 孝生
- 若竹 敏裕
- 佐藤 修二
- 岩間 太
- Will Thomas
東工大旧小林研（2001～2004/9）OB/OG
- 立花 健
- 児玉 紘一
- 海津 智宏
- 大木 憲二
- 松井 宣幸
- 江越 祐紀
- 駒 朋幸
- 原 光太郎
- 白根 和明
- 城 敦