Reference 1
Decompiler: Bestar, IDA Pro as front-end.
translates x86 assembl into PANDA IR (freshly designed).
Symbolic execution engine: leverage framework of GiNac[^c8].
Path Validator and Integer Overflow Checker: STP, a decision procedure for bit-vectors and arrays.
20 zero-day integer overflows in QEMU, Xen, Xine, MPlayer, VLC.
[^c8]
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?