Relational Abstractions Based on Labeled Union-Find
summary
Introduces a data structure that extends union‑find by storing group‑valued labels on parent edges to represent injective relations such as y = ax + b, maintains only a spanning tree so transitive closure avoids cubic costs, and uses path compression to give amortized constant time* find/union operations. It combines with interval, octagon and bitwise domains to factorize variables, runs on SSA, implements joins via Patricia trees with provably optimal precision, and ships working implementations in codeex and collibri with reusable artifacts.
AI-written summary · about
chapters (10)
- 0:00Labeled union-find abstractions
- 1:46Relational abstraction domains
- 3:10Transitive closure assumptions
- 4:35Labeled union-find explained
- 7:02Program analysis with union-find
- 10:33Combining union-find domains
- 13:20Immutability in union-find
- 15:46Loop counters example
- 16:08Conclusion and implementation
- 17:09Q&A
related talks
28mWiP: Labeled Union-Find for Constraint Factorization
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
19mMerging Inductive Relations
18mAssociativity and Commutativity in Equality Saturation
21mRelating Distances and Abstractions: An Abstract Interpretation Perspective
26mA Rule-Based Approach for Designing and Composing Abstract Domains
32mMLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
08mData Structure Abstraction and Incorrectness Separation Logic