Haha yeah that paper is how I got started reversing VM based schemes. A short paper that does use symbolic execution and theorem proving is BinHunt, although it

Haha yeah that paper is how I got started reversing VM based schemes. A short paper that does use symbolic execution and theorem proving is BinHunt, although it's a blatant ripoff of Halvar published 4 years later. Their only claimed contributions are (1) symbolic execution and theorem proving for basic block equivalence and (2) backtracking for their maximum common subgraph isomorphism algorithm (in contrast to Halvar who I believe used direction instruction comparison for basic block equivalence and a greedy subgraph algorithm). These could be meaningful contributions but they provide no data to prove that that the posited accuracy increase of symbolic execution and backtracking is worth the large performance hit.