Constrained Horn Clauses Satisfiability via Catamorphic Abstractions
summary
A terminating unfolding/folding transformation removes algebraic-data-type arguments from Constrained Horn Clauses by encoding user-specified catamorphism-based abstractions and folding them back into ADT-free clauses; the transformation is satisfiability-preserving and targets lists and trees. The implementation emits SMT-LIB input consumed by Z3 and Eldarica. On a benchmark of 75 verification problems the transformed problems yield about +70 additional satisfiable proofs (solver times typically <1s) while the transformation itself runs in under a second.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:23Constrained Horn clauses in verification
- 3:21CHCs in program verification
- 5:34Algebraic data types challenges
- 7:45Catamorphisms in this context
- 11:22Extending catamorphisms
- 13:14Catamorphisms for ADT sorts
- 16:59Transformation process
- 24:12Benchmark results
- 29:19Advantages and limitations
- 30:22Future directions
- 32:38Q&A
related talks
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
29mADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
30mSemantics-Guided Synthesis
23mHigher-Order MSL Horn Constraints
27mCompiling higher-order specifications to SMT solvers: how to deal with rejection ...
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
21mBoosting Constrained Horn Solving by Unsat Core Learning
40mReasoning Under Uncertainty in SMT Solving, Research, and Life