Solving Constrained Horn Clauses over Algebraic Data Types

on YouTube ↗23m

" summary

Implements a solver called AdtChc that synthesizes recursive functions from CHCs over algebraic data types using equality propagation and a new-fun transform, then checks validity with structural-induction backends (AdtInd or Vampire). The pipeline extracts recurrence relations, filters and proves lemmas (lemma filtering and SMT-backed refutation), and requires occasional user Eureka lemmas. Evaluated on 71 benchmarks, the toolset yields the best aggregate coverage (Vampire with structural induction) while AdtInd is substantially faster but less complete.

AI-written summary · about

" chapters (13)

1. 0:00Introduction
2. 1:26Linked list example
3. 3:38ADTs formal encoding
4. 5:27CHCs systems explained
5. 7:16ADTs solving challenges
6. 9:02Recursive invariant algorithm
7. 12:40Algorithm step-by-step
8. 16:14Append function walkthrough
9. 17:38Implementation details
10. 18:20ADT IND solver
11. 20:30Lemma filtering
12. 21:33Evaluation results
13. 22:36Conclusion