研究室案内

国立情報学研究所 (NII) 渡邉研は2025年4月に発足した新しい研究室です。 大学院生を募集しておりますので、ぜひ興味がある方はお気軽にkazukiwatanabe at nii.ac.jpまでご連絡ください。

研究テーマ

ソフトウェアやプログラムの確実な安全性保証技術(モデル検査など)に関して研究しています。 具体的な研究テーマとしては主に、

1. 数学的抽象論によるモデル検査及びプログラム検証の基礎理論の構築
2. 最適化手法による効率的な形式検証手法の開発

テーマ1: モデル検査及びプログラム検証の基礎理論

• 　これまでの(渡邉が関わっている)研究成果の一部
1. Watanabe, Ikebuchi, Kori (ICFP2026) Adequacy for Predicate Transformer Semantics.
2. Kori, Watanabe (CONCUR2026) From Coalgebraic Determinization to Belief Construction for Partial Observability.
3. Kori, Watanabe (FoSSacS2026) A No-go Theorem for Coalgebraic Product Construction.
4. Kori, Watanabe, Rot (LICS2025) Initial Algebra Correspondence under Reachability Conditions
5. Watanabe, Junges, Rot, Hasuo (OOPSLA2025) A Unifying Approach to Product Constructions for Quantitative Temporal Inference
6. Kori, Watanabe, Rot, Katsumata (LICS2024) Composing Codensity Bisimulations
7. Watanabe, Eberhart, Asada, Hasuo (CAV2023) Compositional Probabilistic Model Checking with String Diagrams of MDPs

テーマ2: 効率的な形式検証手法の開発

• 　これまでの(渡邉が関わっている)研究成果の一部
1. Watanabe, Unno (IJCAI-ECAI2026) Automated Safety Verification of Posterior Distributions of Probabilistic Programs
2. Matsumoto, Watanabe, Waga (EMSOFT2026) Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking
3. Matsumoto, Watanabe, Suenaga, Waga (EMSOFT2025) Efficient Black-Box Checking with Specification-Guided Abstraction
4. Watanabe, van der Vegt, Junges, Hasuo (CAV2024) Compositional Value Iteration with Pareto Caching
5. Watanabe, van der Vegt, Hasuo, Rot, Junges (TACAS2024) Pareto Curves for Compositionally Model Checking String Diagrams of MDPs

進学案内

総合研究大学院大学（総研大）情報学コースの5年一貫制博士課程または博士後期課程の学生として、渡邉を指導教員に選ぶことができます。 私(渡邉)自身も、総研大の5年一貫制博士課程の卒業生(2025/03)ですので、学生生活に関して何か質問等あれば遠慮なくお聞きください。 また、渡邉研を希望する場合は、必ず事前に渡邉まで連絡してください(kazukiwatanabe at nii.ac.jp)。