Relational program logics allow reasoning about two programs or two runs of the same program. They provide an elegant means to prove correctness of compiler optimizations or equivalence between two implementations of an abstract data type, and a unifying formalism for specifying and verifying properties like non-interference or determinism. Yet the current technology for relational verification remains underdeveloped. We provide an abstract theory of product programs that supports a direct reduction of relational verification to standard verification. We illustrate the benefits of our method with a state-of-the-art optimization for incremental computation, and with standard examples of loop optimizations. All examples have been verified using the Why framework for program verification.

In this talk I will try to present the main notions of the work through examples without going into many technical details.