Dynamic Symbolic Execution for Software Bug Finding

In this talk, I will give an overview of our work on designing dynamic symbolic execution techniques for comprehensively testing real programs. I will discuss the main challenges of dynamic symbolic execution in terms of path exploration, constraint solving, and interaction with the environment, and our experience building two practical symbolic execution tools, EXE and KLEE, capable of automatically generating high-coverage test inputs exposing serious bugs and security vulnerabilities in a diverse set of software systems, including file systems, device drivers, packet filters, networking servers and computer vision code.