1 citations · 6 across the 8 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.LO2021★ 1 cited
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…