G. Barthe, J. M. Crespo, and C. Kunz, Relational Verification Using Product Programs, International Symposium on Formal Methods, pp.200-214, 2011.
DOI : 10.1007/978-3-540-68237-0_5
URL : http://software.imdea.org/~jmcrespo/docs/FM2011.pdf

G. Barthe, J. M. Crespo, and C. Kunz, Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification, International Symposium on Logical Foundations of Computer Science, pp.29-43, 2013.
DOI : 10.1007/978-3-642-35722-0_3
URL : http://software.imdea.org/~jmcrespo/docs/LFCS2013.pdf

G. Barthe, J. M. Crespo, and C. Kunz, Product programs and relational program logics, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.5, pp.847-859, 2016.
DOI : 10.1016/j.jlamp.2016.05.004

G. Barthe, B. Grégoire, J. Hsu, and P. Strub, Coupling proofs are probabilistic product programs, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp.161-174, 2017.
DOI : 10.1145/3093333.3009896
URL : https://hal.archives-ouvertes.fr/hal-01649028

N. Benton, Simple Relational Correctness Proofs for Static Analyses and Program Transformations (Revised, Long Version), 2005.
DOI : 10.1145/964001.964003

J. Brunel, D. Doligez, R. Rydhof-hansen, J. L. Lawall, and G. Muller, A foundation for flow-based program matching: using temporal logic and model checking, In Acm Sigplan Notices, vol.441, pp.114-126, 2009.
DOI : 10.1145/1480881.1480897
URL : https://hal.archives-ouvertes.fr/hal-00297708

J. Cohen, Renaming Global Variables in C Mechanically Proved Correct, Proceedings of the Fourth International Workshop on Verification and Program Transformation, 2016.
DOI : 10.1109/CSMR.2003.1192417
URL : https://hal.archives-ouvertes.fr/hal-01277269

T. Girka, D. Mentré, and Y. Régis-gianas, A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences, International Symposium on Automated Technology for Verification and Analysis, pp.64-79, 2015.
DOI : 10.1007/978-3-319-24953-7_6
URL : https://hal.archives-ouvertes.fr/hal-01238704

T. Girka, D. Mentré, and Y. Régis-gianas, Coq development. https://www.irif.fr/~thib, 2017.

C. Hawblitzel, M. Kawaguchi, S. Lahiri, and H. Rebelo, Mutual Summaries: Unifying Program Comparison Techniques, 2011.

L. Lamport and M. Abadi, The existence of refinement mappings, Proceedings of the 3rd Annual Symposium on Logic in Computer Science, pp.165-175, 1988.

D. Park, Concurrency and automata on infinite sequences, Theoretical computer science, pp.167-183, 1981.
DOI : 10.1007/BFb0017309

N. Partush and E. Yahav, Abstract semantic differencing via speculative correlation, In ACM SIGPLAN Notices, pp.49-59, 2014.
DOI : 10.1145/2714064.2660245

S. Person, B. Matthew, S. Dwyer, C. S. Elbaum, and . P?as?areanup?as?p?as?areanu, Differential symbolic execution, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, SIGSOFT '08/FSE-16, pp.226-237, 2008.
DOI : 10.1145/1453101.1453131
URL : http://esquared.unl.edu/articles/downloadArticle.php?id=270

C. Hawblitzel, S. Lahiri, and K. Mcmillan, Differential Assertion Checking, 2013.

T. Hoare, S. Lahiri, and K. Vaswani, Differential Static Analysis: Opportunities, Applications, and Challenges, 2010.

G. Soares, R. Gheyi, and T. Massoni, Automated Behavioral Testing of Refactoring Engines, IEEE Transactions on Software Engineering, vol.39, issue.2, pp.147-162, 2013.
DOI : 10.1109/TSE.2012.19

O. Strichman and B. Godlin, Regression Verification - A Practical Way to Verify Programs, Working Conference on Verified Software: Theories, Tools, and Experiments, pp.496-501, 2005.
DOI : 10.1007/BFb0054170
URL : http://iew3.technion.ac.il/~ofers/publications/grand-challenge.pdf