53 citations · 154 across the 20 of their papers we have counts for
21 papers
On Higher-Order Reachability Games vs May Reachability
Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with an…
Automatic HFL(Z) Validity Checking for Program Verification
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato +1
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reducti…
An Overview of the HFL Model Checking Project
Naoki Kobayashi
In this article, we give an overview of our project on higher-order program verification based on HFL (higher-order fixpoint logic) model checking. After a brief introduction to HF…
Termination Analysis for the -Calculus by Reduction to Sequential Program Termination
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi +3
We propose an automated method for proving termination of -calculus processes, based on a reduction to termination of sequential programs: we translate a -calculus process to…
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
Takumi Shimoda, Naoki Kobayashi, Ken Sakayori +1
Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT…
Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes
Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi
We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution tim…