Sato, Ryosuke

NameSato, Ryosuke

氏名佐藤亮介

PositionAssociate Professor, Information Media Center

AffiliationTokyo University of Agriculture and Technology

DoctorateTohoku University, 2013

Emailrsato [at] acm.org

ORCID0000-0001-8679-2747

DBLPRyosuke Sato 0001

Software

maintained

since
2011

MoCHi

Software Model Checker for Higher-Order Programs

Web demo Repository

Journal Papers

10 papers

2026

Solvable Tuple Patterns and Their Applications to Program Verification

Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka

Proceedings of the ACM on Programming Languages, Vol. 10, Issue PLDI, Article 180, pp. 277–302DOI
2024

Asynchronous Unfold/Fold Transformation for Fixpoint Logic

Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato

Science of Computer Programming 231:103014DOI
2023

Higher-order Property-Directed Reachability

Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato

Proceedings of the ACM on Programming Languages, Vol. 7, Issue ICFP, Article 190, pp. 48–77DOI
Refinement types for call-by-name programs

Ryosuke Sato

Journal of Information Processing, Vol. 31, 708–721DOI
HFL(Z) Validity Checking for Automated Program Verification

Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada

Proceedings of the ACM on Programming Languages, Vol. 7, Issue POPL, Article 6, pp. 154–184DOI
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, Naoyasu Ubayashi

Information and Software Technology 146:106855DOI
2020

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs

Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato

Journal on Automated Reasoning 64(7): 1393–1418DOI
2017

Verifying relational properties of functional programs by first-order refinement

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

Science of Computer Programming 137: 2–62DOI
2015

Refinement Type Checking via Assertion Checking

Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

Journal of Information Processing 23(6): 827–834DOI PDF
2011

Ordered Types for Stream Processing of Tree-Structured Data

Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi

Journal of Information Processing 19: 74–87DOI

Conference Papers

28 papers

2025

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types

Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

The 32nd Static Analysis Symposium (SAS 2025)
On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic

Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

The 34th European Symposium on Programming (ESOP 2025)Distinguished Paper Award
2024

Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem

Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

The 22nd Asian Symposium on Programming Languages and Systems (APLAS 2024)
Productivity Verification for Functional Programs by Reduction to Termination Verification

Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato

ACM SIGPLAN 2024 Workshop on Partial Evaluation and Program Manipulation (PEPM 2024)
Borrowable Fractional Ownership Types for Verification

Takashi Nakayama, Yusuke Matsushita, Ryosuke Sato, Ken Sakayori, Naoki Kobayashi

The 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024)
2023

Argument Reduction of Constrained Horn Clauses Using Equality Constraints

Ryo Ikeda, Ryosuke Sato, Naoki Kobayashi

The 21st Asian Symposium on Programming Languages and Systems (APLAS 2023)
Gradual Tensor Shape Checking

Momoko Hattori, Naoki Kobayashi, Ryosuke Sato

The 32nd European Symposium on Programming (ESOP 2023)
2022

Parameterized Recursive Refinement Types for Automated Program Verification

Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato

The 29th Static Analysis Symposium (SAS 2022)
Asynchronous Unfold/Fold Transformation for Fixpoint Logic

Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato

The 16th International Symposium on Functional and Logic Programming (FLOPS 2022)
2021

Termination Analysis for the Pi-Calculus by Reduction to Sequential Program Termination

Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada

The 19th Asian Symposium on Programming Languages and Systems (APLAS 2021)arXiv
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

The 28th Static Analysis Symposium (SAS 2021), Chicago, Illinois, USAarXiv Artifact
Inside-Outside Algorithm for Macro Grammars

Ryuta Kambe, Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka

Proceedings of Machine Learning Research 153 (PMLR 2021)
2020

How Fast and Effectively Can Code Change History Enrich Stack Overflow?

Ryujiro Nishinaka, Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato

The 20th IEEE International Conference on Software Quality, Reliability, and Security (QRS 2020), Macau, China
2019

When and Why Do Software Developers Face Uncertainty?

Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato

The 19th IEEE International Conference on Software Quality, Reliability, and Security (QRS 2019), Sofia, Bulgaria
Combining Higher-Order Model Checking with Refinement Type Inference (short paper)

Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi

ACM SIGPLAN 2019 Workshop on Partial Evaluation and Program Manipulation (PEPM 2019), Cascais/Lisbon, PortugalPDF Benchmarks
2018

HoIce: An ICE-based Non-Linear Horn Clause Solver (tool paper)

Adrien Champion, Naoki Kobayashi, Ryosuke Sato

The 16th Asian Symposium on Programming Languages and Systems (APLAS 2018), Wellington, New ZealandPDF
iArch-U/MC: An Uncertainty-Aware Model Checker for Embracing Known Unknowns

Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato

The 13th International Conference on Software Technologies (ICSOFT 2018), Porto, Portugal
ICE-based Refinement Type Discovery for Higher-Order Functional Programs

Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato

The 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Thessaloniki, Greece
Exploring uncertainty in GitHub OSS projects: when and how do developers face uncertainty?

Naoyasu Ubayashi, Hokuto Muraoka, Daiki Muramoto, Yasutaka Kamei, Ryosuke Sato

The 40th International Conference on Software Engineering: Companion Proceedings (ICSE 2018), Gothenburg, Sweden
Can Abstraction Be Taught? Refactoring-based Abstraction Learning

Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato

The 6th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2018), Funchal, Madeira, Portugal
2017

Modular Verification of Higher-order Functional Programs

Ryosuke Sato, Naoki Kobayashi

The 26th European Symposium on Programming (ESOP 2017), Uppsala, SwedenPDF Benchmarks
2016

Automatically Disproving Fair Termination of Higher-Order Functional Programs

Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

The 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Nara, JapanPDF
Temporal Verification of Higher-order Functional Programs

Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

The 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), St. Petersburg, FloridaPDF
2015

Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs

Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

The 27th International Conference on Computer Aided Verification (CAV 2015), San Francisco, CaliforniaPDF
Verifying Relational Properties of Functional Programs by First-Order Refinement

Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi

ACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM 2015), Mumbai, IndiaShort version Full version
2013

Towards a Scalable Software Model Checker for Higher-Order Programs

Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM 2013), Rome, Italy
2011

Predicate Abstraction and CEGAR for Higher-Order Model Checking

Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno

The 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011), San Jose, CA, USAPDF
2009

Ordered Types for Stream Processing of Tree-Structured Data

Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi

ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X 2009), Savannah, GA, USAPDF

Talks

3 talks

2019

Combining Higher-Order Model Checking with Refinement Type Inference

Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi

The 8th Asian Workshop on Advanced Software Engineering (AWASE 2019), Fukuoka, Japan
2015

Refinement Type Checking via Assertion Checking

Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

Workshop on Higher-Order Program Analysis, Kyoto, Japan
2012

MoCHi: Software Model Checker for a Higher-Order Functional Language

Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

ACM SIGPLAN Workshop on ML, DenmarkPDF

Poster Presentations

1 poster

2007

Type-Based Partial Buffering for Stream Processing

Ryosuke Sato, Naoki Kobayashi

The 5th Asian Symposium on Programming Languages and Systems (APLAS 2007), Singapore

Professional Activities

20 roles

2026
APLAS 2026Program CommitteePPL 2026Program CommitteeESOP 2026Program CommitteePOPL 2026Program Committee
2025
PLDI 2025External Review Committee
2024
APLAS 2024Publicity Co-ChairICFP 2024Program CommitteeFoSSaCS 2024Artifact Evaluation Committee Chair
2023
APLAS 2023Publicity ChairJSSST 40th Annual Conf.Vice Organizing Committee ChairPPL 2023Program Committee
2022
PPL 2022Program Committee
2021
PPL 2021Organizing Committee
2020
APLAS 2020Local Arrangement ChairPPL 2020Organizing Chair
2019
PPL 2019Organizing Committee
2017
PPL 2017Program CommitteePEPM 2017Program Committee
2016
PPL 2016Program Committee
2015
HOPA 2015Program Committee

Teaching

8 courses

2020–2025Software Engineering II (Guest Lecture)Kyushu University
2021–2023Programming LanguagesWaseda University
2021–2022Experiments of Functional/Logic Programming (in Japanese)The University of Tokyo
2020–2022Experiments of Compiler (in Japanese)The University of Tokyo
2019–2020Basic Information Utilization (in Japanese)Seinan Gakuin University
2017–2020Project-Based Learning (in Japanese)Kyushu University
2017–2020Experiments of Software (in Japanese)Kyushu University
2019Advanced Information Processing (in Japanese)Seinan Gakuin University

Software

MoCHi

Journal Papers

Solvable Tuple Patterns and Their Applications to Program Verification

Asynchronous Unfold/Fold Transformation for Fixpoint Logic

Higher-order Property-Directed Reachability

Refinement types for call-by-name programs

HFL(Z) Validity Checking for Automated Program Verification

An empirical study on self-admitted technical debt in modern code review

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs

Verifying relational properties of functional programs by first-order refinement

Refinement Type Checking via Assertion Checking

Ordered Types for Stream Processing of Tree-Structured Data

Conference Papers

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types

On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic

Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem

Productivity Verification for Functional Programs by Reduction to Termination Verification

Borrowable Fractional Ownership Types for Verification

Argument Reduction of Constrained Horn Clauses Using Equality Constraints

Gradual Tensor Shape Checking

Parameterized Recursive Refinement Types for Automated Program Verification

Asynchronous Unfold/Fold Transformation for Fixpoint Logic

Termination Analysis for the Pi-Calculus by Reduction to Sequential Program Termination

Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

Inside-Outside Algorithm for Macro Grammars

How Fast and Effectively Can Code Change History Enrich Stack Overflow?

When and Why Do Software Developers Face Uncertainty?

Combining Higher-Order Model Checking with Refinement Type Inference (short paper)

HoIce: An ICE-based Non-Linear Horn Clause Solver (tool paper)

iArch-U/MC: An Uncertainty-Aware Model Checker for Embracing Known Unknowns

ICE-based Refinement Type Discovery for Higher-Order Functional Programs

Exploring uncertainty in GitHub OSS projects: when and how do developers face uncertainty?

Can Abstraction Be Taught? Refactoring-based Abstraction Learning

Modular Verification of Higher-order Functional Programs

Automatically Disproving Fair Termination of Higher-Order Functional Programs

Temporal Verification of Higher-order Functional Programs

Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs

Verifying Relational Properties of Functional Programs by First-Order Refinement

Towards a Scalable Software Model Checker for Higher-Order Programs

Predicate Abstraction and CEGAR for Higher-Order Model Checking

Ordered Types for Stream Processing of Tree-Structured Data

Talks

Combining Higher-Order Model Checking with Refinement Type Inference

Refinement Type Checking via Assertion Checking

MoCHi: Software Model Checker for a Higher-Order Functional Language

Poster Presentations

Type-Based Partial Buffering for Stream Processing

Professional Activities

Teaching