The S2E verifier can analyze application code, complex GUI libraries, kernel code, device drivers, and even hardware devices. It does this by alternating between concrete execution (using QEMU) and symbolic execution (using the KLEE verifier). Switching modes makes it more flexible but it also makes it more efficient because (slower) symbolic execution can be restricted to the code of most interest which might be a library, a recently changed code path, etc.
The big trick is switching from concrete execution to symbolic execution.
The evaluation is fairly sparse but they say they are able to analyze device drivers in Windows with only a 1.7x slowdown relative to unmodified QEMU.