 Conference Article[zwingend]  Sabine Glesner, Wolf Zimmermann, Structural Simulation Proofs based on ASMs even for NonTerminating Programs, Proceedings of the ASMWorkshop, Eight International Conference on Computer Aided Systems Theory EUROCAST 2001, Feb 2001.

AbstractWhen transforming programs, one often has the requirement to preserve
their semantics, as e.g. in compilers. To guarantee that such a
requirement is fulfilled, formal proofs are necessary. Therefore, we
want to do a simulation proof by showing that the state transitions
which appear when running the original and the transformed program,
resp., are the same. In a first attempt, one could try an inductive
simulation proof over the number of these state transitions. But, as we
show here, this approach does not work in general. Induction is fine as
long as programs terminate. But for nonterminating programs it is not
appropriate. In this paper, we show that a coinductive proof technique
is necessary in principle and that the problem of simulation proofs for
nonterminating programs can be solved easily using coinduction.
Authors
 