Sato, Ryosuke (佐藤 亮介)

Ph.D. Tohoku University, 2013.

Associate Professor (Information Media Center, Tokyo University of Agriculture and Technology)

https://orcid.org/0000-0001-8679-2747

DBLP: Ryosuke Sato 0001

Software

• MoCHi: Software Model Checker for Higher-Order Programs [Web demo][Repository]

Journal Papers

• Asynchronous Unfold/Fold Transformation for Fixpoint Logic
  Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
  Science of Computer Programming. 231:103014 (2024).
  https://doi.org/10.1016/j.scico.2023.103014
• Higher-order Property-Directed Reachability
  Hiroyuki Katsura, Naoki Kobayashi, Ryosuke Sato
  Proceedings of the ACM on Programming Languages. Volume 7, Issue ICFP, Article No. 190, pp 48–77. 2023.
  https://doi.org/10.1145/3607831
• Refinement types for call-by-name programs
  Ryosuke Sato
  Journal of Information Processing. Vol 31, 708–721 (2023).
  https://doi.org/10.2197/ipsjjip.31.708
• HFL(Z) Validity Checking for Automated Program Verification
  Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada
  Proceedings of the ACM on Programming Languages. Volume 7, Issue POPL, Article No. 6, pp. 154–184. 2023.
  https://doi.org/10.1145/3571199
• 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: 106855 (2022).
  https://doi.org/10.1016/j.infsof.2022.106855
• 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–1418 (2020).
  https://doi.org/10.1007/s10817-020-09571-y
• Verifying relational properties of functional programs by first-order refinement.
  Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi.
  Science of Computer Programming. 137: 2–62 (2017).
  https://doi.org/10.1016/j.scico.2016.02.007
• Refinement Type Checking via Assertion Checking.
  Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi.
  Journal of Information Processing. 23(6): 827–834 (2015).
  https://doi.org/10.2197/ipsjjip.23.827
  [PDF]
• Ordered Types for Stream Processing of Tree-Structured Data.
  Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi.
  Journal of Information Processing. 19: 74–87 (2011).
  https://doi.org/10.2197/ipsjjip.19.74

Conference Papers

• On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic
  Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
  In the 34th European Symposium on Programming (ESOP 2025). (To appear)
• Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem
  Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
  In the 22nd Asian Symposium on Programming Languages and Systems (APLAS 2024). 2024.
• Productivity Verification for Functional Programs by Reduction to Termination Verification
  Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato
  In ACM SIGPLAN 2024 Workshop on Partial Evaluation and Program Manipulation (PEPM 2024). 2024.
• Borrowable Fractional Ownership Types for Verification
  Takashi Nakayama, Yusuke Matsushita, Ryosuke Sato, Ken Sakayori, Naoki Kobayashi
  In 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
  In the 21st Asian Symposium on Programming Languages and Systems (APLAS 2023). 2023.
• Gradual Tensor Shape Checking
  Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
  In the 32nd European Symposium on Programming (ESOP 2023). 2023.
• Parameterized Recursive Refinement Types for Automated Program Verification
  Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato
  In the 29th Static Analysis Symposium (SAS 2022). 2022.
• Asynchronous Unfold/Fold Transformation for Fixpoint Logic
  Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
  In the 16th International Symposium on Functional and Logic Programming (FLOPS 2022). 2022.
• Termination Analysis for the Pi-Calculus by Reduction to Sequential Program Termination
  Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
  In the 19th Asian Symposium on Programming Languages and Systems (APLAS 2021). 2021.
  [arXiv]
• Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
  Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
  In the 28th Static Analysis Symposium (SAS 2021), Chicago, Illinois, United States, 2021.
  [arXiv, Artifact]
• Inside-Outside Algorithm for Macro Grammars
  Ryuta Kambe, Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
  In Proceedings of Machine Learning Research 153 (PMLR 2021). 2021.
• How Fast and Effectively Can Code Change History Enrich Stack Overflow?
  Ryujiro Nishinaka, Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato.
  In the 20th IEEE International Conference on Software Quality, Reliability, and Security (QRS 2020), Macau, China, 2020.
• When and Why Do Software Developers Face Uncertainty?
  Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato.
  In the 19th IEEE International Conference on Software Quality, Reliability, and Security (QRS 2019), Sofia, Bulgaria, 2019.
• Combining Higher-Order Model Checking with Refinement Type Inference (short paper).
  Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi.
  In ACM SIGPLAN 2019 Workshop on Partial Evaluation and Program Manipulation (PEPM 2019), Cascais/Lisbon, Portugal, 2019.
  [PDF, Benchmark programs]
• HoIce: A ICE-based Non-Linear Horn Clause Solver (tool paper).
  Adrien Champion, Naoki Kobayashi, Ryosuke Sato.
  In the 16th Asian Symposium on Programming Languages and Systems (APLAS 2018), Wellington, New Zealand, 2018.
  [PDF]
• iArch-U/MC: An Uncertainty-Aware Model Checker for Embracing Known Unknowns.
  Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato.
  In the 13th International Conference on Software Technologies (ICSOFT 2018), Porto, Portugal, 2018.
• ICE-based Refinement Type Discovery for Higher-Order Functional Programs.
  Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato.
  In the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Thessaloniki, Greece, 2018.
• Exploring uncertainty in GitHub OSS projects: when and how do developers face uncertainty?
  Naoyasu Ubayashi, Hokuto Muraoka, Daiki Muramoto, Yasutaka Kamei, Ryosuke Sato.
  In the 40th International Conference on Software Engineering: Companion Proceeedings (ICSE 2018), Gothenburg, Sweden, 2018.
• Can Abstraction Be Taught? Refactoring-based Abstraction Learning.
  Naoyasu Ubayashi, Yasutaka Kamei, Ryosuke Sato.
  In the 6th International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2018), Funchal, Madeira - Portugal, 2018.
• Modular Verification of Higher-order Functional Programs.
  Ryosuke Sato, Naoki Kobayashi.
  In the 26th European Symposium on Programming (ESOP 2017), Uppsala, Sweden, 2017.
  [PDF, Benchmark programs]
• Automatically Disproving Fair Termination of Higher-Order Functional Programs.
  Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi.
  In the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Nara, Japan, 2016.
  [PDF]
• Temporal Verification of Higher-order Functional Programs.
  Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno.
  In the 43th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), St. Petersburg, Florida, 2016.
  [PDF]
• Predicate Abstraction and CEGAR for Disproving Termination of Higher-order Functional Programs.
  Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi.
  In the 27th International Conference on Computer Aided Verification (CAV 2015), San Francisco, California, 2015.
  [PDF]
• Verifying Relational Properties of Functional Programs by First-Order Refinement.
  Kazuyuki Asada, Ryosuke Sato, Naoki Kabayashi.
  In ACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM 2015), Mumbai, Italy, January 2015.
  [Short-version, Full-version]
• Towards a Scalable Software Model Checker for Higher-Order Programs.
  Ryosuke Sato, Hiroshi Unno, Naoki Kabayashi.
  In ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM 2013), Rome, Italy, January 2013.
• Predicate Abstraction and CEGAR for Higher-Order Model Checking.
  Naoki Kabayashi, Ryosuke Sato, Hiroshi Unno.
  In the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2011), San Jose, CA, USA, June 2011.
  [PDF]
• Ordered Types for Stream Processing of Tree-Structured Data.
  Ryosuke Sato, Kohei Suenaga, Naoki Kobayashi.
  In ACM SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X 2009), Savannah, GA, USA, January 2009.
  [PDF]

Talks

• 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, October 2019.
• Refinement Type Checking via Assertion Checking.
  Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi.
  Workshop on Higher-Order Program Analysis, Kyoto, Japan, July 2015.
• MoCHi: Software Model Checker for a Higher-Order Functional Language.
  Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi.
  ACM SIGPLAN Workshop on ML, Denmark, September 2012.
  [PDF]

Poster presentation

• Type-Based Partial Buffering for Stream Processing.
  Ryosuke Sato, Naoki Kobayashi.
  The Fifth ASIAN Symposium on Programming Languages and Systems (APLAS 2007), Singapore, December 2007.

Professional Activities

• APLAS 2024: Publicity Co-Chair
• ICFP 2024: Program Committee
• FoSSaCS 2024: Artifact Evaluation Committee Chair
• APLAS 2023: Publicity Chair
• The 40th JSSST Annual Conference: Vice Organizing Committee Chair
• PPL 2023: Program Committee
• PPL 2022: Program Committee
• PPL 2021: Organizing Committee
• APLAS 2020 : Local Arrangement Chair
• PPL 2020 : Organizing Chair
• PPL 2019 : Organizing Committee
• PPL 2017 : Program Committee
• PEPM 2017 : Program Committee
• PPL 2016 : Program Committee
• HOPA 2015 : Program Committee

Teaching Activities

• Programming Languages. WASEDA University. 2021–2023.
• Experiments of Functional/Logic Programming (In Japanese). The University of Tokyo. 2021–2022.
• Experiments of Compiler (In Japanese). The University of Tokyo. 2020–2022.
• Basic Information Utilization (In Japanese). Seinan Gakuin University. 2019–2020.
• Project-Based Learing (In Japanese). Kyushu University. 2017–2020.
• Experiments of Software (In Japanese). Kyushu University. 2017–2020.
• Advanced Information Processing (In Japanese). Seinan Gakuin University. 2019.