Practical Aspects of Loop Semantics Recovery
Practical Aspects of Loop Semantics Recovery

Summary/Abstract: Revealing the meaning of a given program (reverse engineering) can be a challenging task, especially if the intended purpose is unknown and the source code is poorly documented. The full information about what a procedural program computes is captured by its denotational semantics, which could be difficult and cumbersome to formulate precisely. Nevertheless, program properties which are proven correct could provide useful hints of the meaning of a program, even if weaker or incomplete. Loop invariants are examples of such properties, and there exist several methods for automating the task of finding a correct invariant for a given loop. Symbol elimination is one such technique which requires no additional information or prior knowledge about the program. In the present paper we investigate the practical aspects for revealing of program properties by utilizing Lingva — a software tool for invariant generation via the symbol elimination method.

• Details
• Contents