Formal methods for practical reverse engineering and software verification