Using Informal and Formal Techniques for the Reverse Engineering of C Programs