Categorical Semantics of Probabilistic Symbolic Execution
summary
Builds a denotational universe where symbolic execution is a presheaf model and proves a single metatheorem: any definitional interpreter written in the internal language of the resulting category of symbolic sets (presheaves) yields a correct symbolic semantics for its ordinary set interpretation. Extends to state merging by using mergeable symbolic sets (sheaves) and correctness via instantiation structures (gluing). Produces an executable Haskell reference interpreter, explains why list merging matches RoSEtTE’s length-based merge, and ships reusable artifacts.
AI-written summary · about
chapters (9)
- 0:00Probabilistic symbolic execution intro
- 1:04How probabilistic symbolic execution works
- 3:28Motivation for categorical semantics
- 6:16Category of symbolic sets
- 10:50Symbolic metal language and constructions
- 13:37State merging with mergeable sets
- 16:26Sheaf semantics and topology
- 18:13Correctness via instantiation
- 20:19Q&A
related talks
16mCompositional Symbolic Execution for the Next 700 Memory Models
15mSemantics of Sets of Programs
49mSemantic Foundations for Probabilistic Programming
16mCompiling Symbolic Execution with Staging and Algebraic Effects
21mChecking Equivalence in a Non-strict Language
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
25mSymbolic Bisimulation for Open and Parameterized Systems
15mStable Relations and Abstract Interpretation of Higher-Order Programs