Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding

Explore a 14-minute video presentation from the PLDI 2024 conference on a novel approach to symbolic execution for efficient bug finding. Learn about the compatible branch coverage driven technique that addresses the path explosion problem in symbolic execution. Discover how this method uses program dependency analysis to create a path-pruning strategy, effectively avoiding unnecessary explorations. Understand the concept of Compatible Branch Set and how it directs symbolic execution to explore feasible branches while pruning redundant paths. Examine the implementation of this approach using KLEE and its performance in experiments on programs from Siemens Suite, GNU Coreutils, and other real-world applications. Gain insights into the significant improvements achieved, including over 45% path reduction and 3x speedup on GNU Coreutils programs compared to state-of-the-art techniques. Access supplementary materials, including reusable artifacts, to further explore this innovative approach to program analysis and software testing.