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…