It was just explained to me by a prominent security company that "symbolic execution" is the same thing as "dynamic taint analysis."