Verification of ASM refinements using generalized forward simulation
This paper describes a generic proof method for the correctness of refinements of Abstract State Machines based on commuting diagrams. The method generalizes forward simulations from the refinement of I/O automata by allowing arbitrary m: n diagrams, and by combining it with the refinement of data structures.
refinement forward simulation abstract state machines commuting diagrams data refinement transition systems i/o-automata dynamic logic correctness proofs interactive theorem proving compiler verification