Key Design Points
The most important design question for constructing the constraint formula is to figure out what instructions to include in the formula. We need to include all the instructions for an exploitable path for the solver to generate a candidate exploit. However, the number of exploitable paths is usually only a fraction of all paths to the new check. Should the formula cover all such execution paths, some of them, or just one? We consider three approaches to answering this question: a dynamic approach which considers only a single path at a time, a static approach which considers multiple paths in the CFG without enumerating them, and a combined dynamic and static approach.

This is a really good example of combining Static Analysis and Dynamic Analysis to find and verify security vulnerabilities. Come see my Summercon presentation for more on this topic.

RE: Automatic Patch-Based Exploit Generation is Possible: Techniques and Implications