5 citations · 6 across the 3 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
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…
cs.LO2022★ 1 cited
On Higher-Order Reachability Games vs May Reachability
Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with an…