[Japanese Version]
Kobayashi Laboratory
Dept. of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo
News
- A paper based on Nakayama-san's senior thesis "Borrowable Fractional Ownership Types for Verification" was accepted to VMCAI 2024.
- A paper based on Fukaishi-san's master thesis "Productivity Verification for Functional Programs by Reduction to Termination Verification" was accepted to PEPM 2024.
- A paper based on Tanaka-san's senior thesis "Ownership Types for Verification of Programs with Pointer Arithmetic" was accepted to PEPM 2024.
- A paper that extends the work of Katsura-san's master thesis "Higher-Order Property-Directed Reachability" was accepted to ICFP 2023.
- A paper that extends the work of Hattori-san's master thesis "Gradual Tensor Shape Checking" was accepted to ESOP 2023.
- A paper that extends the work of Tanahashi-san's master thesis "HFLz Validity Checking for Automated Program Verification" was accepted to POPL 2023.
- A paper that extends the work of Mukai-san's senior thesis "Parameterized Recursive Refinement Types for Automated Program Verification" was accepted to SAS 2022.
- A paper based on Matsushita-san's master thesis "RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code" was accepted to PLDI 2022 (with Distinguished Paper Award).
Introduction
Our research group is studying theoretical foundations for software and their applications such as program verification. On the one hand, an increasing number of important systems such as transportation systems, medical devices, and banking systems are now controlled by computer software, and a bug of such software can cause a serious disaster. On the other hand, such software is becoming more and more complex and larger, and it is difficult to maintain the quality of software by using traditional software engineering technologies like testing. In view of these situations, we aim to improve the reliability and efficiency of software by developing automated techniques for program verification and transformation based on rigorous mathematical methods. To achieve the goal, we also need to study and advance many research topics in theoretical computer science, such as type theory, formal languages and automata, and automated theorem proving. It is a pleasure of our research to find out that deep mathematical results, which initially seem to be only of theoretical interests, are actually quite useful for the practically-motivated research mentioned above.
Recent research topics include:
- Higher-order model checking:
This is an extension of traditional model checking that has been successfully applied to system verification. We have recently constructed the first higher-order model checker in the world.
- Automated program verification: By applying the higher-order model checking mentioned above, we are developing fully-automated program verification tools for programming languages like ML and Java.
- Data compression: String and tree data can be compressed in the form of programs that generate them. The higher-order model checking above can be used to transform such compressed data without decompression.
To Foreign Students Who Wish to Study in Our Group
See this page.
Members
Staffs
Students
- Shin Saito (D3)
- Hiroyuki Katsura (D3)
- Yu Sasaki (D2)
- Takahiro Ishikawa (D2)
- Izumi Tanaka (M2)
- Takashi Nakayama (M2)
- Yurika Hirobe (M2)
- Joe Hattori (M2)
- Musashi Katsura (M1)
- Junwei Wang (M1)
Alumni
Alumni of Kobayashi Lab @ University of Tokyo (—2000, Apr. 2012—)
- Atsushi Igarashi (Professor, Kyoto University)
- Eijiro Sumii (Professor, Tohoku University)
- Kazutaka Matsuda (Associate Professor, Tohoku University)
- Hiroshi Unno (Associate Professor, Tsukuba University)
- Takeshi Tsukada (Associate Professor, Chiba University)
- Ryoma Shin-ya (Assistant Professor, Akita University)
- Kazuyuki Asada (Assistant Professor, Tohoku University)
- Yoshiki Nakamura (Assistant Professor, Tokyo Institute of Technology)
- Adrien Champion
- Christopher Broadbent
- Sohei Ito (Associate Professor, Nagasaki University)
- Xin Li
- Mahmudul FAISAL Al Ameen
- Ryousuke Sato (Associate Professor, Tokyo University of Agriculture and Technology)
- Yusuke Matsushita
- Kohei Asano
- Ren Fukaishi
- Risa Yamada
- Koichi Imai
- Keisuke Nishimura
- Ryo Ikeda
- Tsubasa Shoshi
- Ryoya Mukai
- Hideto Ueno
- Ryuta Kambe
- Kento Tanahashi
- Momoko Hattori
- Liu Yuxi
- Koki Ryu
- Yulu Pan
- Kentaro Honda
- Takayuki Niki
- Takumi Shimoda
- Takuma Ishikawa
- Naoki Iwayama
- Shingo Eguchi
- Hiroki Oshikawa
- Yo Mitani
- Mayuko Kori
- Natsuki Urabe
- Taku Terao
- Tanti Kaveri
- Yuki Imai
- Ryota Suzuki
- Ibuki Okamoto
- Yuya Okumura
- Takashi Suwa
- Kengo Kido
- Masaki Hara
- Takamasa Okudono
- Yuta Arichi
- Keiichi Watanabe
- Zhengyi Lu
- Yuta Nagata
- Tomoya Chiba
- Anders Kiel Hovgaard
- Chinmay Mahesh Chandak
- Sadaaki Kawata
- Kotaro Takeda
- Kazuhide Yasukata
- Koichi Fujima
- Takuya Kuwahara
- Yuma Matsumoto
- Masata Kida
- Yuto Takei
- Toshihiro Shimizu
- Akihiro Kishimoto (IBM Research Lab, Dublin)
- Hideki Kariya
- Shin Saito
- Haruhiko Nakao
Alumni of Kobayashi Lab @ Tohoku University (Oct. 2004—Mar. 2012)
Alumni of Kobayashi Lab @ Tokyo Institute of Technology (2001—Sep. 2004)
- Atsushi Shiro
- Keita Shirane
- Kazuaki Yoshibayashi
- Koutaro Hara
- Tomoyuki Koma
- Hiroki Egoshi
- Nobuyuki Matsui (Fujitsu)
- Kenji Ooki (Tokuda Lab.)
- Tomohiro Kaizu (Tokuda Lab.)
- Kouichi Kodama (Tokyo Institute of Technology)
- Takeshi Tachibana (Tokyo Institute of Technology)