1 citations · 4 across the 5 of their papers we have counts for
4 papers · 1 filter
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…
Toward Neural-Network-Guided Program Synthesis and Verification
Naoki Kobayashi, Taro Sekiyama, Issei Sato +1
We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. We first show that, by suitably designing and training neural networks, we c…
RustHorn: CHC-based Verification for Rust Programs (full version)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointe…