Efficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse
summary
Claims a concolic engine that compiles a CPS-based Wasm concolic interpreter to C++ via partial evaluation (LMS), producing an executable that combines no interpretation overhead with snapshot reuse by capturing continuations as resumable snapshots. Prototype generates C++ runtime plus symbolic ops, runs on small benchmarks and reports 6–15× speedups over Wasp, and the toolchain and source are available on GitHub for further evaluation.
AI-written summary · about
chapters (11)
- 0:00Concolic execution intro
- 1:04Symbolic vs concolic basics
- 4:21Challenges in reuse
- 7:12Interpretation vs instrumentation
- 10:05Compilation to reduce overhead
- 11:27Partial evaluation
- 13:58Staged interpreter details
- 16:47Snapshot reuse implementation
- 17:09Preliminary evaluation
- 17:52Summary and contributions
- 18:13Q&A
