Beyond Fuzzing Symbolic Testing in Practice
summary
Shows how symbolic testing models transferFrom as a control‑flow dungeon, uses SMT solvers to explore every feasible path and produce concrete counterexamples, and finds that transferFrom on a plain ERC‑20 yields only null transfers while a fee on transfer variant violates the “no other balances change” property. Compares costs: fuzzers find 1-in‑a‑million bugs quickly, symbolic testing gives definitive coverage when SMT handles the constraints, but hits path explosion and nonlinear arithmetic limits. Mentions Haros and Foundry‑style property tests.
AI-written summary · about
chapters (10)
- 0:00The dungeon game analogy
- 2:29Understanding symbols
- 4:26Challenges of path exploration
- 5:31Applying property testing
- 10:35Symbolic vs. fuzzy testing
- 12:02Improving test coverage
- 13:33Identifying bugs
- 14:53How solvers work
- 16:40Pragmatic testing strategies
- 18:40Conclusion and tools
related talks
21mModern Testing and Fuzzing in Bitcoin Core
55mMuch ado about testing
18mSMT2Test: From SMT Formulas to Effective Test Cases
52mStructure aware fuzzing
14mVerify, but test: extracting property-based tests from F* specifications
53mThree Colours of Fuzzing: Reflections and Open Challenges
14mModel-guided Fuzzing of Distributed Systems
51mProperty-Based Testing