Abstract

Symbolic execution has gathered a lot of attention in recent years as an effective technique for generating high-coverage test suites and for finding deep errors in complex software applications. In this talk, I will discuss the main challenges of symbolic execution in terms of path exploration and constraint solving, and our experience building two practical symbolic execution tools, EXE and KLEE, which are able to automatically discover serious bugs and security vulnerabilities in a diverse set of software systems, including network servers, file systems, device drivers, packet filters, utility applications, and computer vision code.

Invited talk given at SAT/SMT Summer School 2011.