Error Invariants for Fault Localization via Abstract Interpretation

on YouTube ↗27m

" summary

Presents a concrete technique that computes error invariants by iterating backward and forward abstract-interpretation analyses to shrink an error slice and explain assertion failures. Uses a BDD refinement when if‑guards cause precision loss, calls the Z3 SMT solver to find minimal supporting conjuncts, and ships as an OCaml prototype using Apron and BDD Apron domains. Evaluated on C benchmarks: precision improves over single backward analysis, results are comparable to BugAssist but multiple iterations and large BDD abstract domain sizes increase runtime.

AI-written summary · about

" chapters (13)

1. 0:00Error invariants for fault localization
2. 1:26Error invariants with abstract interpretation
3. 3:39Computing error invariants: assignment example
4. 5:29If statements and precision loss
5. 7:16Refining analysis with BDD domains
6. 8:20While loops and irrelevant variables
7. 9:01Formalizing error invariants
8. 13:41Abstract semantics and refinement
9. 16:22Loop for precise error invariants
10. 18:15Implementation and experiments
11. 20:23Comparing with fault localization tools
12. 21:47Contributions and conclusions
13. 22:34Q&A