Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
summary
Implements a static dependence analysis to compute a Compatible Branch Set that lets symbolic execution soundly prune branches that do not add new branch coverage, implemented on KLEE and evaluated on Siemens Suite, GNU Coreutils, and real-world programs. Claims reproduce bugs using significantly fewer paths (on average 45% path reduction, 3x speedup) while matching or improving branch coverage, and provides artifact links and evaluated reusable artifacts to reproduce results.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:59Large-scale analysis observations
- 3:05Proposed solution
- 5:58Branch dependence and sets
- 8:12State space exploration
- 10:23Experimental results
- 12:54Conclusion
related talks
12mTool Talk: KLEE
19mthe path to achieve a bug-free build on the mainline
20mDerivative-Guided Symbolic Execution
19mFeature-Sensitive Coverage for Conformance Testing of Programming Language Implementations
14mSynchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
52mFinding Bugs Using Path-Sensitive Static Analysis
40mAdvanced Test Coverage Criteria: Specify and Measure, Cover and Unmask
18mSymbolic Execution Explained: Finding Bugs in Complex Code Paths