C. Audebaud and . Paulin-mohring, Proofs of randomized algorithms in Coq, Science of Computer Programming, vol.74, issue.8, pp.568-589, 2009.
DOI : 10.1016/j.scico.2007.09.002
URL : https://hal.archives-ouvertes.fr/inria-00431771

J. Baier and . Katoen, Principles of model checking, 2008.

B. Barthe, S. Grégoire, and . Zanella-béguelin, Formal certification of code-based cryptographic proofs, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.90-101, 2009.

B. Barthe, F. Köpf, S. Olmedo, and . Zanella-béguelin, Probabilistic relational reasoning for differential privacy, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.97-110, 2012.
DOI : 10.1145/2103656.2103670
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.5756

M. Barthe, E. J. Gaboardi, J. Gallego-arias, C. Hsu, P. Kunz et al., Proving Differential Privacy in Hoare Logic, 2014 IEEE 27th Computer Security Foundations Symposium
DOI : 10.1109/CSF.2014.36
URL : http://arxiv.org/abs/1407.2988

T. Barthe, M. Espitau, B. Gaboardi, J. Grégoire, P. Hsu et al., Formal certification of randomized algorithms, 2015.

T. Barthe, B. Espitau, J. Grégoire, L. Hsu, P. Stefanesco et al., Relational Reasoning via Probabilistic Coupling, International Conference on Logic for Programming , Artificial Intelligence and Reasoning (LPAR), pp.387-401, 2015.
DOI : 10.1007/978-3-662-48899-7_27
URL : https://hal.archives-ouvertes.fr/hal-01246719

M. Barthe, B. Gaboardi, J. Grégoire, P. Hsu, and . Strub, Proving Differential Privacy via Probabilistic Couplings, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16
DOI : 10.1145/2933575.2934554
URL : https://hal.archives-ouvertes.fr/hal-01411097

A. Bhat, R. Agarwal, A. Vuduc, and . Gray, A type theory for probability density functions, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.545-556, 2012.
DOI : 10.1145/2103656.2103721

A. D. Borgström, M. Gordon, J. Greenberg, J. V. Margetson, and . Gael, Measure transformer semantics for Bayesian machine learning, 2013. URL http

S. Chakarov and . Sankaranarayanan, Probabilistic program analysis with martingales URL https, International Conference on Computer Aided Verification (CAV), pp.511-526, 2013.
DOI : 10.1007/978-3-642-39799-8_34
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.360.1642

S. Chakarov and . Sankaranarayanan, Expectation Invariants for Probabilistic Program Loops as Fixed Points, International Symposium on Static Analysis (SAS), pp.85-100, 2014.
DOI : 10.1007/978-3-319-10936-7_6

M. Cousot and . Monerau, Probabilistic Abstract Interpretation, European Symposium on Programming (ESOP), pp.169-193, 2012.
DOI : 10.1007/978-3-642-28869-2_9

C. Dwork and A. Roth, The Algorithmic Foundations of Differential Privacy, Foundations and Trends?? in Theoretical Computer Science, vol.9, issue.3-4, pp.14-14211, 2014.
DOI : 10.1561/0400000042

F. Dwork, K. Mcsherry, A. Nissim, and . Smith, Calibrating Noise to Sensitivity in Private Data Analysis, IACR Theory of Cryptography Conference (TCC), pp.265-284, 2006.
DOI : 10.1007/11681878_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.131.9267

M. , F. Fioriti, and H. Hermanns, Probabilistic termination: Soundness, completeness , and compositionality, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.489-501, 2015.

D. Foster, K. Kozen, M. Mamouras, A. Reitblatt, and . Silva, Probabilistic NetKAT, European Symposium on Programming (ESOP), 2016.
DOI : 10.1007/11499169_15

A. Gaboardi, J. Haeberlen, A. Hsu, B. C. Narayan, and . Pierce, Linear dependent types for differential privacy, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.357-370, 2013.
DOI : 10.1145/2429069.2429113
URL : https://hal.archives-ouvertes.fr/hal-00909340

J. Gretz, A. Katoen, and . Mciver, Prinsys???On a Quest for Probabilistic Loop Invariants, International Conference on Quantitative Evaluation of Systems (QEST), pp.193-208, 2013.
DOI : 10.1007/978-3-642-40196-1_17

A. Gupta, J. Roth, and . Ullman, Iterative Constructions and Private Data Release, IACR Theory of Cryptography Conference (TCC), pp.339-356, 2012.
DOI : 10.1007/978-3-642-28914-9_19

G. N. Hardt and . Rothblum, A Multiplicative Weights Mechanism for Privacy-Preserving Data Analysis, 2010 IEEE 51st Annual Symposium on Foundations of Computer Science, pp.61-70, 2010.
DOI : 10.1109/FOCS.2010.85

M. Hart, A. Sharir, and . Pnueli, Termination of probabilistic concurrent programs, ACM Symposium on Principles of Programming Languages (POPL), pp.1-6, 1982.

A. Hurd, C. Mciver, and . Morgan, Probabilistic guarded commands mechanized in HOL, Theoretical Computer Science, vol.346, issue.1, pp.96-112, 2005.
DOI : 10.1016/j.tcs.2005.08.005
URL : http://doi.org/10.1016/j.tcs.2005.08.005

G. D. Jones and . Plotkin, A probabilistic powerdomain of evaluations, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.186-195, 1989.
DOI : 10.1109/LICS.1989.39173

L. Kaminski, J. Katoen, C. Matheja, and F. Olmedo, Weakest Precondition Reasoning for Expected Run???Times of Probabilistic Programs, European Symposium on Programming (ESOP), 2016.
DOI : 10.1007/978-3-642-76771-5

-. Katoen, J. Katoen, A. Mciver, L. Meinicke, and C. Morgan, Perspectives in probabilistic verification Linear-invariant generation for probabilistic programs, International Symposium on Static Analysis (SAS), pp.3-10, 2008.
DOI : 10.1007/978-3-642-15769-1_24

. Kozen, Semantics of probabilistic programs, 20th Annual Symposium on Foundations of Computer Science (sfcs 1979), pp.101-114, 1979.
DOI : 10.1109/SFCS.1979.38

. Kozen, A probabilistic PDL, Journal of Computer and System Sciences, vol.30, issue.2, pp.162-178, 1985.
DOI : 10.1016/0022-0000(85)90012-1
URL : http://doi.org/10.1016/0022-0000(85)90012-1

Z. Kwiatkowska, G. Norman, and D. Parker, Probabilistic symbolic model checking with PRISM: A hybrid approach, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.52-66, 2002.
DOI : 10.1007/3-540-46002-0_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5908

C. Mciver and . Morgan, Abstraction, Refinement, and Proof for Probabilistic Systems, Monographs in Computer Science, 2005.

K. Mcsherry and . Talwar, Mechanism Design via Differential Privacy, 48th Annual IEEE Symposium on Foundations of Computer Science (FOCS'07), pp.94-103, 2007.
DOI : 10.1109/FOCS.2007.66

. Monniaux, Abstract Interpretation of Probabilistic Semantics, International Symposium on Static Analysis (SAS), pp.322-339, 2000.
DOI : 10.1007/978-3-540-45099-3_17

A. Morgan, K. Mciver, and . Seidel, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.325-353, 1996.
DOI : 10.1145/229542.229547

H. Ramshaw, Formalizing the Analysis of Algorithms, 1979.

R. and S. Zdancewic, VPHL: A verified partial-correctness logic for probabilistic programs, Mathematical Foundations of Program Semantics (MFPS), 2015.

B. C. Reed and . Pierce, Distance makes the types grow stronger: A calculus for differential privacy, ACM SIGPLAN International Conference on Functional Programming (ICFP)

P. Sampson, T. Panchekha, K. S. Mytkowicz, D. Mckinley, L. Grossman et al., Expressing and verifying probabilistic assertions, ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), p.14, 2014.
DOI : 10.1145/2666356.2594294
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.456.9986

A. Sharir, S. Pnueli, and . Hart, Verification of Probabilistic Programs, SIAM Journal on Computing, vol.13, issue.2, pp.292-314, 1984.
DOI : 10.1137/0213021