With background in formal logic, our laboratory is seeking for new computational models, developing new methods for analyzing and verifying such models, and implementing new tools for analysis and verification. While our main target is software systems and programming languages, we also deal with molecular and biological systems, and we are currently doing research on molecular computing.
We study theoretical foundations for software, and their applications to programming languages, program verification, and program transformation. The recent topics include automated program verification based on higher-order model checking.
We study various topics in machine learning.
Computational science is a new approach in the science after the experimental and the theoretical approaches and has developed with the exponential evolution of computers. By utilizing the first-principles electronic structure calculation as a core, the laboratory carries out the educations and researches in the interface region between computer science and compuational science.
We employ abstract mathematical languages (esp. category theory and mathematical logic) to model various phenomena in computer science, aiming at fundamental understanding as well as novel applied methods. Current application areas include: formal verification, system correctness, information security, quantum programming, hybrid systems.
Our research interests include operating systems, real-time systems, and parallel and distributed systems, with a particular emphasis on resource management for heterogeneous computing environments composed of many cores, GPUs, and FPGAs. We also work on parallel processing on those processors and its performance analysis. Furthermore, we develop autonomous vehicles, high-definition 3D maps, and online machine learning frameworks.