Unified Compositional Symbolic Execution

on YouTube ↗41m

" summary

Claims a unified engine that combines OX (correctness) and UX (incorrectness) reasoning via an axiomatic interface and parametric consume/produce functions; implements automatic matching plans to reorder and bind separation-logic assertions (unlike Verifast/Viper’s manual ordering). Prototype is the Gillian platform with an HCal core and language backends for JavaScript, C and unsafe Rust. It lifts symbolic errors to source, powers a VS Code symbolic debugger, and already finds real bugs (AWS library bugs reproduced and traced back to source).

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 4:45Theory to practice in symbolic execution
3. 8:23Unified compositional symbolic execution
4. 12:45Engine and interface design
5. 16:09Matching plans in symbolic execution
6. 21:11Function rules for Ox and Ux reasoning
7. 26:12Gillian platform and memory model
8. 30:11Real-world applications
9. 32:03Debugging and visualization
10. 36:02Future directions
11. 39:39Q&A