Reverse Engineering from Assembler to Formal Specifications via Program Transformations