Compiling Symbolic Execution with Staging and Algebraic Effects
summary
Claims a first Futamura projection for symbolic interpreters and shows a pipeline that stages a definitional interpreter (Scala + Freer monads + LMS) to generate C++ symbolic executors linked with STP and an immutable runtime. Prototype handles ~20 LLVM IR instructions, compiles to binaries, and on benchmarks is 10–30× faster than the unstaged interpreter and 2–3× faster than KLEE (a 1M+‑path case finishes in 96s vs KLEE ≈300s; unstaged times out).
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:17Symbolic Execution
- 1:11Building a symbolic compiler is often the most difficult aspect of creating solver-aided tools, especially for general-purpose languages.
- 2:55Our Approach - Overview
- 3:17Our Approach - Definitional Interpreters
- 4:38Our Approach - Symbolic Definitional Interpreter
- 5:45Our Approach - Staged Symbolic Definitional Interpreter
- 10:28Execution Strategies à la Effect Handlers
- 13:28Performance
- 15:14Staged symbolic definitional interpreter with algebraic effects
related talks
29mPartially Evaluating Symbolic Interpreters for All
29mStaging Automatic Differentiation with Fusion
07mFutamura Projections
09mCompilers for nothing, executables for free!
15mStaged Compilation with Two-Level Type Theory
18mCompiling with Abstract Interpretation
46mDr. Futamura and the Projection Machine: From Interpreters to Compilers
01h 01mA partial history of partial evaluation