The S2E verifier is an implementation of the idea of “selective symbolic execution” described in chipounov:hotdep:2009.
The tool can analyze application code, complex GUI libraries, kernel code, device drivers, and even hardware devices. This allows it to analyze Windows kernel code. It does this by alternating between concrete execution (using QEMU) and symbolic execution (using the KLEE verifier).
Papers related to S2E verifier
- S2E: A platform for in-vivo multi-path analysis of software systems [chipounov:asplos:2011]
- Selective symbolic execution [chipounov:hotdep:2009]
- The S2E platform: Design, implementation, and applications [chipounov:tcs:2012]
- Symbolic execution with SymCC: Don't interpret, compile! [poeplau:usenix:2020]