Partially Evaluating Symbolic Interpreters for All
summary
Builds staged symbolic interpreters with Lightweight Modular Staging (LMS) to compile concolic and call‑chain backward symbolic execution for an LLVM‑style IR, generating executables that link a symbolic runtime and SMT backend. A concolic compiler produces results with comparable performance to SymCC on benchmarks; a backward compiler solves cases where forward engines blow up by summarizing functions and traversing call chains. Prototype reuses prior nondeterministic engine, needs about 500 lines of changes and uses Z3/STP for queries.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:28Symbolic Execution Engines
- 2:06Symbolic Compilers
- 2:31Multi-stage programming
- 4:59Concolic Execution
- 6:51Our approach - Concrete Interpreters
- 7:21Our approach - Concolic Interpreters
- 11:56Our approach - Staged Interpreter
- 15:12CCBSE: Call-Chain Backward Symbolic Executio
- 19:01Schedule the order of execution
- 19:39Summaries and compositions
- 21:33This is all we need!
- 22:35Evaluation
- 23:30Conclusion
related talks
16mCompiling Symbolic Execution with Staging and Algebraic Effects
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
09mCompilers for nothing, executables for free!
21mTowards Compiler-Guided Static Analysis
42mDeveloping the Wolfram Language Compiler
27mCompiler Support for Control-Flow Linearization Using Architectural Mimicry
14mHigher-Order Demand-Driven Symbolic Evaluation
20mPartial Evaluation, Whole-Program Compilation