A Formal Automated Approach for Reverse Engineering Programs with Pointers

Given a program S and a precondition Q, the strongest postcondition, denoted sp(S Q), is defined as the strongest condition that holds after the execution of S, given that S terminates. By defining the formal semantics of each of the constructs of a programming language, a formal specification of the behavior of a program written using the given programming language can be constructed. In this paper we address the formal semantics of pointers in order to handle a realistic model of programming languages that incorporate the use of pointers. In addition, we present a tool for supporting the construction of formal specifications of programs that include the use of pointers.

• Type: Conference
• Year: 1997
• Where: KBSE
• Authors: Gerald C. Gannod, Betty H. C. Cheng
• Keywords: Formal Semantics, Formal Specifications, KBSE 1997, Programming Languages, Software Engineering