Abstract

Dynamic symbolic execution has gathered a lot of attention in recent years as an effective technique for generating high-coverage test suites and finding deep errors in complex software applications. In this tutorial, I will discuss the main challenges of symbolic execution in terms of path exploration and constraint solving, and our experience applying this technique in several different contexts, including bug finding, attack generation, patch testing and bounded verification.

Invited tutorial talk given at CAV 2013.