T. Antonopoulos, P. Gazzillo, M. Hicks, E. Koskinen, T. Terauchi et al., Decomposition instead of self-composition for proving the absence of timing channels, Proc. of the 38th SIGPLAN Conference on Programming Language Design and Implementation, pp.362-375, 2017.

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, P. R. D-'argenio, and T. Rezk, Secure information flow by self-composition, Mathematical Structures in Computer Science, vol.4, issue.06, pp.1207-1252, 2011.
DOI : 10.1145/5397.5399

P. Baudin, F. Bobot, L. Correnson, and Z. Dargaye, WP Plugin Manual v1, 2017.

P. Baudin, P. Cuoq, J. C. Filliâtre, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language

N. Benton, Simple relational correctness proofs for static analyses and program transformations, Proc. of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.14-25, 2004.

P. G. Bishop, R. E. Bloomfield, and L. Cyra, Combining testing and proof to gain high assurance in software: A case study, 2013 IEEE 24th International Symposium on Software Reliability Engineering (ISSRE), pp.248-257, 2013.
DOI : 10.1109/ISSRE.2013.6698924

L. Blatter, N. Kosmatov, P. L. Gall, and V. Prevosto, RPP: Automatic Proof of Relational Properties by Self-composition, Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.391-397, 2017.
DOI : 10.1093/comjnl/25.4.465

URL : https://hal.archives-ouvertes.fr/cea-01808885

P. Cuoq, B. Monate, A. Pacalet, and V. Prevosto, Functional dependencies of C functions via weakest pre-conditions, International Journal on Software Tools for Technology Transfer, vol.37, issue.1???3, pp.405-417, 2011.
DOI : 10.1016/S0167-6423(99)00024-6

M. Delahaye, N. Kosmatov, and J. Signoles, Common specification language for static and dynamic analysis of C programs, Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13, pp.1230-1235, 2013.
DOI : 10.1145/2480362.2480593

URL : https://hal.archives-ouvertes.fr/hal-00853721

R. W. Floyd, Assigning meanings to programs, Proc. of the American Mathematical Society Symposia on Applied Mathematics, vol.19, 1967.
DOI : 10.1007/978-94-011-1793-7_4

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, 1969.
DOI : 10.1007/978-3-642-48354-7_17

URL : http://www.utdallas.edu/~kxh060100/cs6371fa07/hoare.pdf

M. Kiefer, V. Klebanov, and M. Ulbrich, Relational Program Reasoning Using Compiler IR, Journal of Automated Reasoning, vol.26, issue.2, pp.337-363, 2018.
DOI : 10.1145/1512475.1512477

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective. Formal Asp, Comput, vol.27, issue.3, pp.573-609, 2015.
DOI : 10.1007/s00165-014-0326-7

URL : https://hal.archives-ouvertes.fr/cea-01808981

K. R. Leino and N. Polikarpova, Verified Calculations, 5th International Conference, on Verified Software: Theories, Tools, Experiments (VSTTE 2013), Revised Selected Papers, pp.170-190, 2013.
DOI : 10.1007/978-3-642-54108-7_9

G. Petiot, B. Botella, J. Julliand, N. Kosmatov, and J. Signoles, Instrumentation of Annotated C Programs for Test Generation, 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation, pp.105-114, 2014.
DOI : 10.1109/SCAM.2014.19

G. Petiot, N. Kosmatov, B. Botella, A. Giorgetti, and J. Julliand, Your Proof Fails? Testing Helps to Find the Reason, Proc. of the 10th International Conference on Tests and Proofs, pp.130-150, 2016.
DOI : 10.1007/11408901_21

URL : https://hal.archives-ouvertes.fr/cea-01808892

J. Signoles, , 2012.

M. Sousa and I. Dillig, Cartesian Hoare Logic for Verifying k-safety Properties, Proc. of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.57-69, 2016.

K. Vorobyov, J. Signoles, and N. Kosmatov, Shadow state encoding for efficient monitoring of block-level properties, Proc. of the International Symposium on Memory Management, pp.47-58, 2017.
URL : https://hal.archives-ouvertes.fr/cea-01836510