Abstract

Constraint solving plays a key role in symbolic execution, an effective and popular technique for testing complex software. In this talk, I will give an overview of symbolic execution, and I will discuss the constraint solving challenges arising in applying symbolic execution to several application domains, including whole-program bug-finding, high-coverage patch testing, testing and verification of performance optimisations, and recovery of broken documents without any prior knowledge of the file format.

Talk given at SMT 2015.