concolic-execution
An analysis tool for Python that blurs the line between testing and type systems.
Ariadne is a binary analysis toolkit for understanding programs that do not want to be understood. It runs a target inside a userspace emulator with real Windows DLLs, then reasons about what it did with symbolic execution.