...

Constraint Solving Challenges in Dynamic Symbolic

...

Execution

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 this approach in terms of constraint solving 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, network servers and computer vision code.

...