[Japanese Version]
Kobayashi Laboratory
Dept. of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo
News
- Tanaka-san has been selected for SPRING GX, a financial support program for PhD students.
- A paper based on Yamada-san's master thesis "On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic" was accepted for ESOP 2025. Moreover, this paper is selected as a Distinguished Paper.
- Nakayama-san won a Poster Award at PPL 2025 (a domestic conference on programming and programming languages).
- A position paper based on Tanaka-san's master thesis "High-Level Synthesis with Linear Types" was accepted for LATTE 2025.
- A paper by Prof. Kobayashi "On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus" was accepted for POPL 2025.
- Prof. Kobayashi gave an (joint) invited talk at ATVA 2024 and APLAS 2024.
- A paper by Katsura et al. "Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem" was accepted for APLAS 2024.
- A paper based on Nakayama-san's senior thesis "Borrowable Fractional Ownership Types for Verification" was accepted for VMCAI 2024.
- A paper based on Fukaishi-san's master thesis "Productivity Verification for Functional Programs by Reduction to Termination Verification" was accepted for PEPM 2024.
- A paper based on Tanaka-san's senior thesis "Ownership Types for Verification of Programs with Pointer Arithmetic" was accepted for PEPM 2024.
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
- Takahiro Ishikawa (D2)
- Izumi Tanaka (D1)
- Musashi Katsura (M2)
- Junwei Wang (M2)
- Takuya Shimizu (M1)
- Konami Shu (M1)
Alumni
Alumni of Kobayashi Lab @ University of Tokyo (—2000, Apr. 2012—)
- Atsushi Igarashi (Professor, Kyoto University)
- Eijiro Sumii (Professor, Tohoku University)
- Hiroshi Unno (Professor, Tohoku University)
- Takeshi Tsukada (Professor, Chiba University)
- Sohei Ito (Associate Professor, Nagasaki University)
- Kazutaka Matsuda (Associate Professor, Tohoku University)
- Ryousuke Sato (Associate Professor, Tokyo University of Agriculture and Technology)
- Ryoma Shin-ya (Assistant Professor, Akita University)
- Kazuyuki Asada (Assistant Professor, Tohoku University)
- Yoshiki Nakamura (Assistant Professor, Science Tokyo)
- Yusuke Matsushita (Program-Specific Assistant Professor, Hakubi Center for Advanced Research, Kyoto University)
- Adrien Champion
- Christopher Broadbent
- Xin Li
- Mahmudul FAISAL Al Ameen
- Hiroyuki Katsura (Postdoctoral Researcher, University of Cambridge)
- Takashi Nakayama
- Yurika Hirobe
- Joe Hattori
- Shin Saito
- Yu Sasaki
- 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
- 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)