activity
20232026
most citedOwnership Types for Verification of Programs with Pointer Arithmetic

1 citations · 2 across the 7 of their papers we have counts for

collaborators
Showing 2025Show all

2 papers · 1 filter

cs.PL2025

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…

cs.LO2025

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…