[Japanese Version]

Kobayashi Laboratory

Dept. of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo

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:

Members

Staffs

Students

Alumni

Alumni of Kobayashi Lab @ University of Tokyo (—2000, Apr. 2012—)

Alumni of Kobayashi Lab @ Tohoku University (Oct. 2004—Mar. 2012)

Alumni of Kobayashi Lab @ Tokyo Institute of Technology (2001—Sep. 2004)