LAB LOGA page on LabLog, a review site (not the lab's official page)
Kobayashi Lab
Machine-translated · View original
A lab that uses mathematical theory to mechanically verify the correctness of software.
AboutAbout the lab
Verifying software correctness through theory.
Kobayashi Lab studies the foundational theory of software and methods for applying it to program verification.
Systems for transportation, healthcare, e-commerce, and more run on software, and defects can lead to serious accidents.
The lab therefore uses mathematical methods to verify and transform programs mechanically, aiming to improve their reliability and performance.
What makes this field fascinating is that theories such as type theory, automata, and theorem proving connect directly to practical applications.
Key terms
- Type theory
- A theory that assigns classifications called "types" to the values and expressions in a program, so that errors can be found before the program is run
- Theorem proving
- Having a computer handle mathematical proofs and mechanically check whether their reasoning is valid
- Model checking
- A verification technique that exhaustively examines all the states a system can take and checks whether it satisfies a specified property
ResearchResearch themes
While many systems are controlled by software, software has grown so large that running tests alone can no longer ensure its quality. The lab works on research that uses mathematical methods to mechanically verify and transform programs, improving their reliability and performance.
*Illustrative imageHigher-Order Model Checking
Model checking examines every possible state of a system to verify its properties. The lab is extending it so that it can also be applied to software written in high-level languages. It has built the world's first higher-order model checker and applies it to the other research themes.
*Illustrative imageAutomatic Program Verification
Using higher-order model checking, the lab builds tools that automatically verify programs written in the functional language ML and the object-oriented language Java.
*Illustrative imageData Compression
This research compresses string and tree-structured data by representing them as the programs that generate them. Using higher-order model checking, it performs operations such as pattern matching on the data while it remains compressed.
*Illustrative imageAutomatic Verification of Communication Protocols
This research automatically verifies whether communication procedures that use cryptography to exchange confidential information such as passwords, as in online shopping, are secure.
MembersFaculty
Kobayashi Lab consists of faculty members, doctoral and master's students, and administrative staff.As of 2026
- ProfessorNaoki KobayashiPublications ↗
- Assistant ProfessorKen SakayoriPublications ↗
VoicesStudent voices
Compiled from answers by students who were in the lab. Ratings and reviews reflect individual students' experiences, not the lab's official views.
Students who take part in an interview may receive a thank-you gift worth ¥1,000, regardless of what they say.
On a 4-point scale, ● marks where students' answers fall
Who is this lab for?
What's great about this lab?
What did you learn after joining?
What's the vibe, and what is the professor like?
Where do graduates go?
RelatedLabs similar to Kobayashi Lab
Sugiyama-Yokoya-Ishida LabFaculty of Science, Department of Information ScienceEstablishing the foundational theory of machine learning, de…
Shinagawa LabFaculty of Science, Department of Information ScienceResearch on system software, including operating systems and…
Kawarabayashi LabFaculty of Science, Department of Information ScienceResearch on algorithms and discrete mathematics
Ma LabFaculty of Science, Department of Information ScienceEngineering and quality assurance of highly reliable AI syst…The information on this page is compiled by the LabLog team from the lab's public information and interviews. For corrections or removal requests, please contact LabLog, not the lab.
Report an errorAbout the images
The top and research theme images are illustrative and were not taken at the lab. They are cropped from Wikimedia Commons images. Cropped CC BY-SA images are provided under the same CC BY-SA license as the original (version shown on each line).
- Top image: “Programming code” Martin Vorel / CC BY-SA 4.0 (cropped)
- Higher-Order Model Checking: “NFSM state diagram” Maggyero / CC BY-SA 4.0 (cropped)
- Automatic Program Verification: “CoqProofOfDecidablityOfEqualityOnNaturalNumbers” Roconnor / Public domain (cropped)
- Data Compression: “HuffmanCodeAlg” Andreas.Roever at German Wikipedia (Original text: Andreas.Roever) / CC BY-SA 3.0 (cropped)
- Automatic Verification of Communication Protocols: “Asymmetric encryption (colored)” Nicobon / CC BY-SA 4.0 (cropped)
- Related lab (杉山・横矢・石田研究室): “T-SNE Embedding of MNIST” Kyle McDonald / CC BY 2.0 (cropped)
- Related lab (品川研究室): “Alx source snippet” Tino / CC BY-SA 4.0 (cropped)
- Related lab (河原林研究室): “Social Network Visualization” Martin Grandjean / CC BY-SA 4.0 (cropped)
- Related lab (馬研究室): “Unmarked Nissan Rogue - Possible Test Autonomous Vehicle - San Francisco, May 2025 04” 9yz / CC BY 4.0 (cropped)
About LabLog
LabLog is a lab review app for students only. Student members at each university interview students in labs and publish what they say. Student voices can only be read by students who sign up with a university email address. Operated by bestiee Inc.
Learn more about LabLog ↗Search engines and AI may reference the basic lab info and rating summaries on this page and the description of LabLog. Student voices are for student members only. Automated collection by programs (scraping, or input to or training of AI) is prohibited under Article 8 of the Terms of Service. If you need data for research or analysis, please contact us.