Predicate abstraction and CEGAR for higher-order model checking. - Naoki Kobayashi 001; Ryosuke Sato 001; Hiroshi Unno 001 (PLDI, 2011)

Ordered Types for Stream Processing of Tree-Structured Data. - Ryosuke Sato 001; Kohei Suenaga; Naoki Kobayashi 001 (J. Inf. Process., 2011)

Towards a scalable software model checker for higher-order programs. - Ryosuke Sato 001; Hiroshi Unno 001; Naoki Kobayashi 001 (PEPM, 2013)

Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs. - Takuya Kuwahara; Ryosuke Sato 001; Hiroshi Unno 001; Naoki Kobayashi 001 (CAV (2), 2015)

Refinement Type Checking via Assertion Checking. - Ryosuke Sato 001; Kazuyuki Asada; Naoki Kobayashi 001 (J. Inf. Process., 2015)

Automatically disproving fair termination of higher-order functional programs. - Keiichi Watanabe; Ryosuke Sato 001; Takeshi Tsukada; Naoki Kobayashi 001 (ICFP, 2016)

Temporal verification of higher-order functional programs. - Akihiro Murase; Tachio Terauchi; Naoki Kobayashi 001; Ryosuke Sato 001; Hiroshi Unno 001 (POPL, 2016)

Modular Verification of Higher-Order Functional Programs. - Ryosuke Sato 001; Naoki Kobayashi 001 (ESOP, 2017)

Verifying relational properties of functional programs by first-order refinement. - Kazuyuki Asada; Ryosuke Sato 001; Naoki Kobayashi 001 (Sci. Comput. Program., 2017)

HoIce: An ICE-Based Non-linear Horn Clause Solver. - Adrien Champion; Naoki Kobayashi 001; Ryosuke Sato 001 (APLAS, 2018)

Exploring uncertainty in GitHub OSS projects: when and how do developers face uncertainty? - Naoyasu Ubayashi; Hokuto Muraoka; Daiki Muramoto; Yasutaka Kamei; Ryosuke Sato 001 (ICSE (Companion Volume), 2018)

iArch-U/MC: An Uncertainty-Aware Model Checker for Embracing Known Unknowns. - Naoyasu Ubayashi; Yasutaka Kamei; Ryosuke Sato 001 (ICSOFT, 2018)

Modular Programming and Reasoning for Living with Uncertainty. - Naoyasu Ubayashi; Yasutaka Kamei; Ryosuke Sato 001 (ICSOFT (Selected Papers), 2018)

Can Abstraction Be Taught? Refactoring-based Abstraction Learning. - Naoyasu Ubayashi; Yasutaka Kamei; Ryosuke Sato 001 (MODELSWARD, 2018)

Git-based integrated uncertainty manager. - Naoyasu Ubayashi; Takuya Watanabe 002; Yasutaka Kamei; Ryosuke Sato 001 (ICSE (Companion Volume), 2019)

Combining higher-order model checking with refinement type inference. - Ryosuke Sato 001; Naoki Iwayama; Naoki Kobayashi 001 (PEPM@POPL, 2019)

When and Why Do Software Developers Face Uncertainty? - Naoyasu Ubayashi; Yasutaka Kamei; Ryosuke Sato 001 (QRS, 2019)

How Fast and Effectively Can Code Change History Enrich Stack Overflow? - Ryujiro Nishinaka; Naoyasu Ubayashi; Yasutaka Kamei; Ryosuke Sato 001 (QRS, 2020)

A Quantitative Study of Security Bug Fixes of GitHub Repositories. - Daito Nakano; Mingyang Yin; Ryosuke Sato 001; Abram Hindle; Yasutaka Kamei; Naoyasu Ubayashi (CoRR, 2020)

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. - Adrien Champion; Tomoya Chiba; Naoki Kobayashi 001; Ryosuke Sato 001 (J. Autom. Reason., 2020)

Termination Analysis for the $$ pi $$-Calculus by Reduction to Sequential Program Termination. - Tsubasa Shoshi; Takuma Ishikawa; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001; Takeshi Tsukada (APLAS, 2021)

Inside-Outside Algorithm for Macro Grammars. - Ryuta Kambe; Naoki Kobayashi 001; Ryosuke Sato 001; Ayumi Shinohara; Ryo Yoshinaka (ICGI, 2021)

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. - Takumi Shimoda; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (SAS, 2021)

Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. - Tsubasa Shoshi; Takuma Ishikawa; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001; Takeshi Tsukada (CoRR, 2021)

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving. - Takumi Shimoda; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (Zenodo, 2021)

Parameterized Recursive Refinement Types for Automated Program Verification. - Ryoya Mukai; Naoki Kobayashi 001; Ryosuke Sato 001 (SAS, 2022)

Automatic HFL(Z) Validity Checking for Program Verification. - Kento Tanahashi; Naoki Kobayashi 001; Ryosuke Sato 001 (CoRR, 2022)

An empirical study on self-admitted technical debt in modern code review. - Yutaro Kashiwa; Ryoma Nishikawa; Yasutaka Kamei; Masanari Kondo; Emad Shihab; Ryosuke Sato 001; Naoyasu Ubayashi (Inf. Softw. Technol., 2022)

Argument Reduction of Constrained Horn Clauses Using Equality Constraints. - Ryo Ikeda; Ryosuke Sato 001; Naoki Kobayashi 001 (APLAS, 2023)

Gradual Tensor Shape Checking. - Momoko Hattori; Naoki Kobayashi 001; Ryosuke Sato 001 (ESOP, 2023)

Polyhedral Clinching Auctions with a Single Sample. - Ryosuke Sato 001 (CoRR, 2023)

Refinement Types for Call-by-name Programs. - Ryosuke Sato 001 (J. Inf. Process., 2023)

HFL(Z) Validity Checking for Automated Program Verification. - Naoki Kobayashi 001; Kento Tanahashi; Ryosuke Sato 001; Takeshi Tsukada (Proc. ACM Program. Lang., 2023)

Higher-Order Property-Directed Reachability. - Hiroyuki Katsura; Naoki Kobayashi 001; Ryosuke Sato 001 (Proc. ACM Program. Lang., 2023)

Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. - Hiroyuki Katsura; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (APLAS, 2024)

Productivity Verification for Functional Programs by Reduction to Termination Verification. - Ren Fukaishi; Naoki Kobayashi 001; Ryosuke Sato 001 (PEPM, 2024)

Borrowable Fractional Ownership Types for Verification. - Takashi Nakayama; Yusuke Matsushita 002; Ken Sakayori; Ryosuke Sato 001; Naoki Kobayashi 001 (VMCAI (2), 2024)

Asynchronous unfold/fold transformation for fixpoint logic. - Mahmudul Faisal Al Ameen; Naoki Kobayashi 001; Ryosuke Sato 001 (Sci. Comput. Program., 2024)

Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem. - Hiroyuki Katsura; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (Zenodo, 2024)

On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic. - Risa Yamada; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (ESOP (2), 2025)

On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic. - Risa Yamada; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (Zenodo, 2025)

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types. - Hiroyuki Katsura; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001 (CoRR, 2025)