Lab Info
Welcome to our lab information page! I am a newly appointed assistant professor at NII in Tokyo, starting in April 2025.
If you are interested in joining us, feel free to reach out to me via email (kazukiwatanabe at nii.ac.jp)!
Some Research Topics (not exclusive)
We study formal verification, including model checking and software verification.
We mostly focus on:
- Logical (or categorical) foundation of formal verification,
- Optimisation and heuristics for efficient verification algorithms.
We provide some details and references below.
If you join us, you will have the opportunity to work on related topics.
Topic1: Logical (or categorical) foundation of formal verification
We focus on generalizing existing methods and developing new ones by abstracting the natural structures that arise in model checking and program verification,
primarily based on category theory and lattice theory.
- Some related references:
- Kori, Watanabe, Rot (LICS2025) Initial Algebra Correspondence under Reachability Conditions
- Watanabe, Junges, Rot, Hasuo (OOPSLA2025) A Unifying Approach to Product Constructions for Quantitative Temporal Inference
- Kori, Watanabe, Rot, Katsumata (LICS2024) Composing Codensity Bisimulations
- Watanabe, Eberhart, Asada, Hasuo (CAV2023) Compositional Probabilistic Model Checking with String Diagrams of MDPs
Topic2: Optimisation and heuristics for efficient verification algorithms
We are working on the development of efficient model checking methods using algorithms from convex optimization and multi-objective optimization.