Dawson Engler is back

I download and read OSDI 2008 paper tonight, and surprise to find that Dawson Engler start to publish paper again.
This time, one of his student publish a paper about test generation of system sofware, a very old but unresolved topic.
Title of this paper is "KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs".
Basically, this paper still follow the old way of EXE,
By using pseudo symbolic simulation to do partial formal symbolic simulation.