Running the program
•Requires a test suite
–Standard test suites are adequate
–Relatively insensitive to test suite (if large enough)
•No guarantee of completeness or soundness
–Useful nonetheless (cf. Purify, ESC, PREfix)
–Complementary to other techniques and tools
[Don’t be too harsh in the comment about test suites here.]
If you don’t have a test suite -- that is, if you can’t run your program or you never have -- then you are likely to have a number of other problems that you should solve first using standard techniques.  (Another way of saying this is that you have to be able to run your program on some inputs.)
I  not sure of the exact properties that make a test suite good for invariant detection.  We want good value coverage.  A test suite that strives for efficiency by executing each statement a minimal number of times would be bad for invariant detection:  Daikon needs multiple executions as a basis for generalization so that there is statistical support for its inferences
Test suite:  I did experiments regarding test suite size and noticed a knee in the curve comparing Daikon output; also not so sensitive to the exact cases in the suite so long as it was large enough.  (I found these experiments somewhat surprising.)
Like any dynamic analysis such as testing, there is no guarantee of completeness or soundness.
Explain why it’s
• not complete:  infinitely many potential invariants
• not sound: no guarantee that test suite fully characterizes all executions:  the fact that something was true for the first 10,000 executions doesn’t guarantee that it will be true on the next one.  However, it is sound on the training data (all the data presented to it).
It may not be complete or sound, but it is useful, which is more important.
Useful nonetheless:  consider testing, Purify, PREfix (an unsound static tool recently bought by Microsoft for $60 million).  PREfix is symbolic execution, not “abstract interpretation”.