No need to summarize the paper.

1) Suppose we wanted to use symbolic execution to detect
buffer overrun vulnerabilities (i.e., array-out-of-bounds
bugs, where the code writes outside the valid range of an
array).  What would you need to add to a symbolic execution
tool to detect these bugs?

2) Suppose we're building a symbolic execution tool that
works on source code, but we don't have the source code for
library functions.  How could we handle these library
functions?  Name one technique we could use.

3) What would you most like to talk about in class?