This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Problem-Reduction Approach to Proving Simulation Between Programs
June 1976 (vol. 2 no. 2)
pp. 87-96
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.
Index Terms:
theorem proving, Correctness, interactive system, microprogram validation, problem reduction, simulation between programs, symbolic execution
Citation:
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
Usage of this product signifies your acceptance of the Terms of Use.