1 citations · 6 across the 8 of their papers we have counts for
8 papers
Solvable Tuple Patterns and Their Applications to Program Verification
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara +1
Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We in…
Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types
Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori +1
We propose a novel approach to satisfiability checking of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). CHC-based automated verification has gained considerable…
Borrowable Fractional Ownership Types for Verification
Takashi Nakayama, Yusuke Matsushita, Ken Sakayori +2
Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recentl…
Gradual Tensor Shape Checking
Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
Tensor shape mismatch is a common source of bugs in deep learning programs. We propose a new type-based approach to detect tensor shape mismatches. One of the main features of our…
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…
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…
A Quantitative Study of Security Bug Fixes of GitHub Repositories
Daito Nakano, Mingyang Yin, Ryosuke Sato +3
Software is prone to bugs and failures. Security bugs are those that expose or share privileged information and access in violation of the software's requirements. Given the seriou…