Inductive Approach to Spacer
summary
Presents a Spacer-like CHC solver derived by structural induction that replaces global quantifier elimination with an iterative, lazy use of model-based projection to avoid the known divergence scenarios; proves where Spacer variants lose refutational completeness, pinpoints the single algorithmic difference versus GPDR, gives fixes that restore termination under the mild theory conditions described, and reports an implemented solver evaluated on CHC-COMP benchmarks with empirical results showing the approach is practical.
AI-written summary · about
chapters (12)
- 0:00CHC solving challenges
- 1:05Cyclic CHC solving
- 2:52GPDR constraint dependencies
- 5:42GPDR vs quantifier elimination
- 7:26Model-based projection in Spacer
- 9:14Nonlinear CHCs in Spacer
- 13:09Inductive divergence prevention
- 14:38Efficiency improvements
- 15:23Conclusion and future work
- 15:43Q&A on CHC theories
- 16:48Generalizing solving algorithms
- 17:29Final Q&A
related talks
30mSemantics-Guided Synthesis
33mSolving constraints during type inference
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
23mInductive Program Synthesis by Meta-Analysis-Guided Hole Filling
15mAn Empirical Study of Partial Deduction for miniKanren
22mCounterexample-Guided Inference of Modular Specifications
23mAn Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs