A Problem-Reduction Approach to Proving Simulation Between Programs
Alexander Birman, William H. Joyner · IEEE Transactions on Software Engineering · 1976
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.