Octagons Revisited - Elegant Proofs and Simplified Algorithms

on YouTube ↗27m

" summary

Provides simplified cubic time closure algorithms for Octagon abstract relations over rationals and integers that avoid introducing auxiliary negation variables, proves correctness by framing domains as 2-projective (stronger than mere 2-decomposability), and shows a concrete counterexample where Floyd–Warshall fails on merely 2-decomposable domains. Uses a constraint-system view, shows Floyd–Warshall with an added initialization computes the greatest solution for 2-projective domains, gives an O(n^3) normalization, an O(m·n^2) incremental update when m clusters change, improves LP-based best transformers for affine assignments, and reports only a small prototype so far.

AI-written summary · about

" chapters (12)

1. 0:00Octagon relational domains
2. 2:29Decomposable domains
3. 5:39Floyd-Warshall counterexample
4. 8:32Normalization via constraints
5. 11:21Proof idea for projective domains
6. 14:34Floyd-Warshall vs constraints
7. 16:18Cubic normalization
8. 17:47TVPI complexity
9. 18:08Guards in projective domains
10. 20:14Linear assignments
11. 23:06Future work
12. 23:56Q&A