kirancodes.me
To Proof Maintenance & Beyond!
ASE 1997

A Formal Automated Approach for Reverse Engineering Programs with Pointers

Gerald C. Gannod, Betty H. C. Cheng

DOI 10.1109/ase.1997.632842dblp

Abstract

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.

BibTeX
@inproceedings{Gannod-Cheng:ASE97,
  author    = {Gerald C. Gannod and
               Betty H. C. Cheng},
  title     = {A Formal Automated Approach for Reverse Engineering Programs with Pointers},
  booktitle = {ASE},
  pages     = {219--226},
  publisher = {{IEEE} Computer Society},
  year      = {1997},
}

Related papers