Relational program logics are formalisms for specifying and verifying properties about two programs or two runs of the same program. 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 technology for relational verification remains underdeveloped. We provide a general notion of product program that supports a direct reduction of relational 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. © 2011 Springer-Verlag.
CITATION STYLE
Barthe, G., Crespo, J. M., & Kunz, C. (2011). Relational verification using product programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6664 LNCS, pp. 200–214). https://doi.org/10.1007/978-3-642-21437-0_17
Mendeley helps you to discover research relevant for your work.