Relational verification using product programs

Abstract. Relational program logics are formalisms for specifying and verifying properties about two programs or two runs of the same pro-gram. These properties range from correctness of compiler optimizations or equivalence between two implementations of an abstract data type, to properties like non-interference or determinism. Yet the current tech-nology for relational verification remains underdeveloped. We provide a general notion of product program that supports a direct reduction of re-lational verification to standard verification. We illustrate the benefits of our method with selected examples, including non-interference, standard loop optimizations, and a state-of-the-art optimization for incremental computation. All examples have been verified using the Why tool.