Abstract

Symbolic execution has gathered significant interest in recent years as an effective technique for finding deep errors in complex software applications. In this tutorial, I will give an overview of modern dynamic symbolic execution techniques, discuss their key challenges in terms of path exploration, constraint solving, and memory modeling, and present 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, such as network servers, file systems, device drivers, packet filters, utility applications, and computer vision code.

Invited tutorial given at <a href=”http://qav.cs.ox.ac.uk/spin2012/invited.php>SPIN 2012. Please email me for the slides.