symbex

An alternative is S2E (https://s2e.systems), it combines KLEE and QEMU to enable whole-system symbolic execution. It is most suitable when you have a program binary that heavily interacts with the system (system code, device drivers, etc.). S2E does not require writing any syscall models to run programs. This is important from a practical point of view: first, if your program can run in QEMU, it will run on S2E, and second, you will not run into issues of clobbering execution states that you have in KLEE when calling external functions that don't have a model. Of course, S2E is not magic and is still facing path explosion challenges, but you have flexible ways of managing it via a powerful plugin architecture. E.g., you can instrument the guest to use function models, control when to concretize data or prevent execution from forking, writing searcher heuristics, etc.