Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Funct

on YouTube ↗25m

" summary

Presents an IC3/PDR-inspired solver called Racer that combines relationification, controlled unfolding of recursive definitions, and uninterpreted-function abstractions to keep queries decidable while preserving counterexample discovery; guarantees progress and termination with a counterexample for unsafe CHCs modulo ADTs and recursive functions (a class of RDFs called catamorphisms). Implemented inside Z3 on top of Spacer, evaluated on RustHorn and Leon benchmarks, and reports better coverage and bug-finding than several prior CHC solvers.

AI-written summary · about

" chapters (13)

1. 0:00Intro
2. 0:22Automatic program verification
3. 2:29Algorithmic Verification as CHC solving
4. 3:46Constrained Horn Clauses
5. 4:57Solutions to CHCS (inductive invariants of programs)
6. 7:30Encoding RF applications in CHCS
7. 8:56Challenge: RFs are hard!!!!
8. 10:35Typical approach: Relationification CHC CHC
9. 12:01Solving CHCs modulo ADTs and RFs
10. 13:20RF abstraction
11. 14:56UF abstraction
12. 15:41SPACER
13. 19:09Experimental results