1 citations · 6 across the 8 of their papers we have counts for
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…