Symbolic Execution with Separating Decision Diagrams
summary
Defines separating decision diagrams as a zero-suppressed BDD variant that encodes star/or separation-logic formulas by treating atoms (pure or spatial) as ZDD elements, yielding a canonical DAG representation. Implements union, join and separating-conjunction operations as memoized recursive routines that produce proof DAGs and compute frames/remainders directly on the DD without DNF expansion. Empirical inspection over large codebases shows frequent exponential-size savings from sharing, though the implementation is promising but not yet production-robust.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:48Origins of separating decision diagrams
- 2:53Reading decision diagrams
- 4:41Binary and zero-suppressed decision diagrams
- 6:48Why ZDDs matter
- 8:11Heap analysis and DNF limits
- 9:57Defining separating decision diagrams
- 11:23Operations on separating decision diagrams
- 13:11Disjunction and separating conjunction
- 14:54Symbolic execution with decision diagrams
- 17:02Frame inference and proof DAGs
- 18:06Non-determinism and incompleteness
- 18:47Future directions
- 20:12Reflections and standards
- 21:38BDDs, SAT solvers, pitfalls
- 22:43Frame inference limits
- 24:04Q&A
related talks
21mWeighted Context-Free-Language Ordered Binary Decision Diagrams
14mHigher-Order Demand-Driven Symbolic Evaluation
22mImplementing separation logic using an SMT-backed Frame Rule
19mCausality and Semantic Separation
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
20mInductive diagrams for causal reasoning
17mAn Algebra of Sequential Decision Problems
22mCategorical Semantics of Probabilistic Symbolic Execution