2 papers
cs.PL2026
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…