A Counterexample-Guided Debugger for Non-Recursive Datalog
summary
Prototype debugs non-recursive Datalog by (1) a property language for pre/postconditions, (2) a counterexample generator that encodes rule evaluation symbolically and queries an SMT/symbolic solver, and (3) an interactive dialog-based debugger that uses stratified partitions and why/why-not provenance to ask a few targeted questions. Validation proves correctness first; failing cases yield concrete inputs. Implementation is a CLI prototype integrated with SMT backends; many benchmarks produce counterexamples in ≈1 minute while some larger cases time out.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:23Datalog view updates
- 4:09Debugging non-recursive Datalog
- 9:11Counterexample generation
- 14:48Debugger interface
- 19:56Implementation results
- 21:00Conclusion
related talks
17mInteractive Debugging of Datalog Programs
26mDebugging Large-Scale Datalog: A Scalable Provenance Evaluation Strategy
21mLive Verification in an Interactive Proof Assistant
17mBring Your Own Data Structures to Datalog
37mThe Bright Future of Debuggers: Challenges and Opportunities
13mA Drag-and-Drop Proof Tactic
57mVariant analysis
38mFrom the Exorcist to Hercule Poirot