Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
summary
A procedure automatically abstracts CHCs over algebraic data types to integer CHCs by synthesizing catamorphisms (generalized folds) via a CEGAR-style loop that turns solver counterexamples into template constraints and solves them with a CEGIS+testing backend; implementation named Catalia uses linear templates and a portfolio version ChocoCatalia; Catalia solves the most satisfiable ADT instances on CHC-COMP 2024 benchmarks and ChocoCatalia wins ADT‑LIA at CHC‑COMP 2025, showing practical inductive invariant discovery.
AI-written summary · about
chapters (10)
- 0:00CHC verification over ADTs
- 1:50Problem with CHC solvers over ADTs
- 3:57Why ADTs make CHC solving hard
- 5:22Catamorphisms as abstractions
- 7:30Abstraction with catamorphisms
- 9:58Counterexample refinement method
- 11:47Implementation and evaluation
- 13:15Comparison with solvers
- 14:20Conclusion and future work
- 15:21Q&A on templates
related talks
38mConstrained Horn Clauses Satisfiability via Catamorphic Abstractions
29mADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
30mSemantics-Guided Synthesis
22mTurning Catala into a Proof Platform for the Law
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
37mGoing bananas with recursion schemes for fixed point data types
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction
28mElements of Logic Programming in a Concatenative Functional Language