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. ,
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
Secure information flow by self-composition, Mathematical Structures in Computer Science, vol.4, issue.06, pp.1207-1252, 2011. ,
DOI : 10.1145/5397.5399
WP Plugin Manual v1, 2017. ,
ACSL: ANSI/ISO C Specification Language ,
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. ,
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
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
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
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
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
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
Relational Program Reasoning Using Compiler IR, Journal of Automated Reasoning, vol.26, issue.2, pp.337-363, 2018. ,
DOI : 10.1145/1512475.1512477
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
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
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
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
, , 2012.
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. ,
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