Secure Information Flow by Self- Composition, Computer Security Foundations, CSF'04, pp.100-114, 2004. ,
DOI : 10.1109/csfw.2004.1310735
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.378.849
Formal certification of code-based cryptographic proofs, Principles of Programming Languages, POPL'09, pp.90-101, 2009. ,
Relational Verification Using Product Programs, Formal Methods, 2011. ,
DOI : 10.1007/978-3-540-68237-0_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.476.8936
Computer-Aided Security Proofs for the Working Cryptographer, Advances in Cryptology ? CRYPTO 2011, pp.71-90, 2011. ,
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075
Simple relational correctness proofs for static analyses and program transformations, Principles of Programming Languages, POPL'04, pp.14-25, 2004. ,
DOI : 10.1145/982962.964003
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.4900
Logical, metric, and algorithmic characterisations of probabilistic bisimulation, 2011. ,
Optimal markovian couplings and applications, Acta Mathematica Sinica, vol.14, issue.3, pp.260-275, 1994. ,
DOI : 10.1080/17442508608833419
Coupling, Stationarity, and Regeneration, 2000. ,
DOI : 10.1007/978-1-4612-1236-2
Optimal transport: old and new, 2008. ,
DOI : 10.1007/978-3-540-71050-9
Relational separation logic, Theoretical Computer Science, vol.375, issue.1-3, pp.308-334, 2007. ,
DOI : 10.1016/j.tcs.2006.12.036
URL : http://doi.org/10.1016/j.tcs.2006.12.036
CoVaC: Compiler Validation by Program Analysis of the Cross-Product, Formal Methods, pp.35-51, 2008. ,
DOI : 10.1007/978-3-540-68237-0_5