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:
- Watanabe, Ikebuchi, Kori (ICFP2026) Adequacy for Predicate Transformer Semantics.
- Kori, Watanabe (CONCUR2026) From Coalgebraic Determinization to Belief Construction for Partial Observability.
- Kori, Watanabe (FoSSacS2026) A No-go Theorem for Coalgebraic Product Construction.
- 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 formal verification methods. We are particularly interested in developing efficient verification methods for probabilistic systems or probabilistic programs.
- Some related references:
- Watanabe, Unno (IJCAI-ECAI2026) Automated Safety Verification of Posterior Distributions of Probabilistic Programs
- Matsumoto, Watanabe, Waga (EMSOFT2026) Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking
- Matsumoto, Watanabe, Suenaga, Waga (EMSOFT2025) Efficient Black-Box Checking with Specification-Guided Abstraction
- Watanabe, van der Vegt, Junges, Hasuo (CAV2024) Compositional Value Iteration with Pareto Caching
- Watanabe, van der Vegt, Hasuo, Rot, Junges (TACAS2024) Pareto Curves for Compositionally Model Checking String Diagrams of MDPs