Correctness Witness Validation by Abstract Interpretation

on YouTube ↗18m

" summary

Introduces a concrete unassume operator that injects witness invariants into an abstract interpreter to relax state information deliberately, implemented in the Goblin framework and using Apron for octagons/polyhedra; manual correctness witnesses cut CPU time by 7–47% on multi‑threaded benchmarks, and model‑checker witnesses guide the analyzer to prove properties it could not infer alone. The paper gives a dual‑narrowing design for relational domains, a propagating unassume for non‑relational/pointer cases, and empirical precision and performance results.

AI-written summary · about

" chapters (15)

1. 0:00Correctness witness validation intro
2. 1:03Witness validation basics
3. 2:25Abstract interpretation basics
4. 3:29Verification goals with witnesses
5. 3:49Interval analysis example
6. 5:14Relaxing invariants with unassume
7. 6:21Soundness of unassume operators
8. 7:25Relational abstractions handling
9. 8:48Dual narrowing for precision
10. 9:31Backwards evaluation for unassume
11. 11:18Goblin framework implementation
12. 12:00Precision evaluation results
13. 13:02Performance evaluation results
14. 13:45Contributions and conclusion
15. 14:27Q&A