Derivative-Guided Symbolic Execution
summary
Framework builds a symbolic execution for functional code that calls opaque, effectful libraries, encoding LTLf specs as symbolic finite automata and using symbolic derivatives to underapproximate precondition states. Implementation (Hatch, in Camo) runs on 10 ADT implementations with 30 injected bugs and finds most violations in 1–2 seconds; it outperforms a naive SE and a recent verification baseline by orders of magnitude and succeeds on benchmarks where both baselines time out or run out of memory.
AI-written summary · about
chapters (8)
- 0:00Derivative-guided symbolic execution
- 0:27Invalid list structure detection
- 3:39Derivatives guide path exploration
- 7:11Safe executions with symbolic automata
- 9:43Computing derivatives for program points
- 13:01Evaluating with Hatch
- 15:08Conclusion and future work
- 15:51Q&A: Unsafe paths and semantics
related talks
01h 01mSymbolic Execution in .NET
34mSymbolic Execution for Randomized Programs
14mCompatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
18mSymbolic Execution Explained: Finding Bugs in Complex Code Paths
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
21mTrace-Guided Synthesis of Effectful Test Generators
17mSignature Inference for Functional Property Discovery
15mUnifying Execution of Imperative Generators and Declarative Specifications