Folks interested in symbolic execution: there’s active research in making it scale up! S2E won the best-paper award at ASPLOS 2011 for introducing a technique they call selective symbolic execution.
Also interesting: BitBlaze, which applies symbolic execution to detect security vulnerabilities in object code (i.e., compiled binaries).