One particular instance of reasoning about the semantic correctness of programs is to prove that two programs in fact are equivalent, where the notion of equivalence may be relativized w.r.t. the set of observations of interest to be made about the behavior of the code.

In general, proving equivalence is an intriguing problem. The tutorial at MOD 2015 gave a non-exhaustive overview over various techniques in the field. In a first lecture, the tutorial considered the most simple form of programs, namely, straight-line programs which are the basis of, e.g., grammar-based compression schemes.

The second and third lecture then considered document processors which transform structured input into (possibly unstructured) output. Even if these processors are finite-state, elaborate techniques from commutative algebra are required to obtain effective decision procedures.

Finally, the fourth lecture considered observational equivalence of programs in general. Based on a formulation as a hyper-safety property a framework was presented which allows to apply techniques from relational abstract interpretation to infer equivalences in non-trivial cases.

In order to provide a homogeneous presentation of original results, we concentrate in these lecture notes on formalisms where effective decision procedures can be provided, namely, on deterministic top-down tree transducers with and without structured output.