| 2026 | CAV | Automatic Detection of Reference Counting Bugs in Linux Kernel Drivers. | Joe Hattori, Naoki Kobayashi, Ken Sakayori |
| 2026 | CONCUR | Prophecy-Based Automated Verification of Message-Passing Programs. | Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, Ken Sakayori |
| 2026 | CONCUR | Concurrent Visibility: Higher-Order Concurrency with First-Order Store. | Iwan Qumerais, Guilhem Jaber, Ken Sakayori, Davide Sangiorgi |
| 2026 | ESOP | Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators. | Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi |
| 2026 | LICS | Wiring the π-Calculus to Denotational Semantics. | Ken Sakayori, Davide Sangiorgi, Simon Castellan, Pierre Clairambault |
| 2025 | ESOP | On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic. | Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato |
| 2025 | SAS | Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types. | Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato |
| 2024 | APLAS | Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. | Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato |
| 2024 | PEPM | Ownership Types for Verification of Programs with Pointer Arithmetic. | Izumi Tanaka, Ken Sakayori, Naoki Kobayashi |
| 2024 | VMCAI | Borrowable Fractional Ownership Types for Verification. | Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi |
| 2023 | LICS | Extensional and Non-extensional Functions as Processes. | Ken Sakayori, Davide Sangiorgi |
| 2021 | APLAS | Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination. | Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada |
| 2021 | FSCD | Output Without Delay: A π-Calculus Compatible with Categorical Semantics. | Ken Sakayori, Takeshi Tsukada |
| 2021 | SAS | Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. | Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato |
| 2019 | ESOP | A Categorical Model of an \mathbf i/o -typed \pi -calculus. | Ken Sakayori, Takeshi Tsukada |
| 2017 | FOSSACS | A Truly Concurrent Game Model of the Asynchronous \pi -Calculus. | Ken Sakayori, Takeshi Tsukada |