Issue No.02 - June (1976 vol.2)
A. Birman , IBM Thomas J. Watson Research Center
System correctness often presents itself as the problem of showing that two programs, the "specification" and the "implementation," are in some sense equivalent. Such a concept of equivalence is supplied by Milner's definition of simulation between programs. This paper presents a problem-reduction approach to proving simulation, and describes an interactive system designed for this purpose.
theorem proving, Correctness, interactive system, microprogram validation, problem reduction, simulation between programs, symbolic execution
A. Birman, W.H. Joyner, "A Problem-Reduction Approach to Proving Simulation Between Programs", IEEE Transactions on Software Engineering, vol.2, no. 2, pp. 87-96, June 1976, doi:10.1109/TSE.1976.233535