Domain Precision in Galois Connection-less Abstract Interpretation

on YouTube ↗33m

" summary

Shows that completeness of an abstract interpretation is equivalent to abstract non‑interference, letting completeness be checked as a hyperproperty of the program rather than of the analyzer. Develops a deductive system and a hyper‑static analyzer that verifies that property and so decides completeness, reuses complete‑shell/core constructions, and crucially works for weak (non‑Galois) domains like convex polyhedra or automata because monotonicity is not required. Demonstration: a static verifier is built and shown to succeed on representative examples.

AI-written summary · about

" chapters (18)

1. 0:00Domain precision in abstract interpretation
2. 1:06Program correctness in safety-critical systems
3. 3:36False alarms in program analysis
4. 5:50Sources of imprecision in abstract computation
5. 8:01Checking completeness via static analysis
6. 9:04Abstract interpretation without Galois connections
7. 12:19Weak domains and abstraction functions
8. 15:13Weak abstract interpretation framework
9. 17:26Deriving static analysis for completeness
10. 19:57Completeness as program hyper property
11. 22:11Abstract non-interference and completeness
12. 23:38Complete shell for weak domains
13. 24:43Deductive system for abstract interference
14. 25:47Hyper analysis for abstract non-interference
15. 26:31Analyzer properties as program hyper properties
16. 27:37Future work on local completeness
17. 29:48Quantitative abstract non-interference
18. 30:35Q&A