  We propose an operationally-based deductive proof method for program
equivalence. It is based on encoding the language semantics as logically
constrained term rewriting systems (LCTRSs) and the two programs as terms. The
main feature of our method is its flexibility. We illustrate this flexibility
in two applications, which are novel. For the first application, we show how to
encode low-level details such as stack size in the language semantics and how
to prove equivalence between two programs operating at different levels of
abstraction. For our running example, we show how our method can prove
equivalence between a recursive function operating with an unbounded stack and
its tail-recursive optimized version operating with a bounded stack. This type
of equivalence checking can be used to ensure that new, undesirable behavior is
not introduced by a more concrete level of abstraction. For the second
application, we show how to formalize read-sets and write-sets of symbolic
expressions and statements by extending the operational semantics in a
conservative way. This enables the relational verification of program schemas,
which we exploit to prove correctness of compiler optimizations, some of which
cannot be proven by existing tools. Our method requires an extension of
standard LCTRSs with axiomatized symbols. We also present a prototype
implementation that proves the feasibility of both applications that we
propose.
