G. Barthe, T. Espitau, L. Ferrer-fioriti, and J. Hsu, Synthesizing Probabilistic Invariants via Doob???s Decomposition, CAV '16, pp.43-61, 2016.
DOI : 10.1017/CBO9780511813658

O. Bouissou, E. Goubault, J. Goubault-larrecq, and S. Putot, A generalization of p-boxes to affine arithmetic, Computing, vol.4, issue.2, pp.189-201, 2012.
DOI : 10.1016/0888-613X(90)90022-T

O. Bouissou, E. Goubault, S. Putot, A. Chakarov, and S. Sankaranarayanan, Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities, TACAS '16, pp.225-243, 2016.
DOI : 10.1007/978-3-662-49674-9_13

A. Chakarov and S. Sankaranarayanan, Probabilistic Program Analysis with Martingales, CAV '13, 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

A. Chakarov and S. Sankaranarayanan, Expectation Invariants for Probabilistic Program Loops as Fixed Points, SAS '14, pp.85-100, 2014.
DOI : 10.1007/978-3-319-10936-7_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.671.4172

L. Chen, A. Miné, J. Wang, and P. Cousot, An Abstract Domain to Discover Interval Linear Equalities, VMCAI'10, pp.112-128, 2010.
DOI : 10.1007/978-3-642-11319-2_11
URL : https://hal.archives-ouvertes.fr/hal-00531563

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, pp.84-97, 1978.
DOI : 10.1145/512760.512770

P. Cousot and M. Monerau, Probabilistic Abstract Interpretation, ESOP '12, pp.169-193, 2012.
DOI : 10.1007/978-3-642-28869-2_9

R. Cousot, Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles, Thèse d'État ès sciences mathématiques, 1985.

D. Pierro, A. Wiklicky, and H. , Concurrent constraint programming, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '00, pp.127-138, 2000.
DOI : 10.1145/351268.351284

J. Feret, Abstract Interpretation-Based Static Analysis of Mobile Ambients, SAS '01, pp.412-430, 2001.
DOI : 10.1007/3-540-47764-0_24
URL : https://hal.archives-ouvertes.fr/inria-00527929

A. Grïßlinger, Extending the Polyhedron Model to Inequality Systems with Non-linear Parameters using Quantifier Elimination, 2003.

E. Hahn, H. Hermanns, and L. Zhang, Probabilistic reachability for parametric Markov models, International Journal on Software Tools for Technology Transfer, vol.1, issue.1, pp.3-19, 2011.
DOI : 10.1007/s10009-010-0146-x
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.184.3136

B. Jeannet and A. Miné, Apron: A Library of Numerical Abstract Domains for Static Analysis, CAV '09, pp.661-667, 2009.
DOI : 10.1007/978-3-642-02658-4_52
URL : https://hal.archives-ouvertes.fr/hal-00786354

M. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, CAV '11, pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035

L. Gall, T. Jeannet, and B. , Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification, SAS '07, pp.52-68, 2007.
DOI : 10.1007/978-3-540-74061-2_4

D. Lesens, N. Halbwachs, and P. Raymond, Automatic verification of parameterized networks of processes, Theoretical Computer Science, vol.256, issue.1-2, pp.113-144, 2001.
DOI : 10.1016/S0304-3975(00)00104-3
URL : https://hal.archives-ouvertes.fr/hal-00198649

P. Mardziel, S. Magill, M. Hicks, and M. Srivatsa, Dynamic Enforcement of Knowledge-Based Security Policies, 2011 IEEE 24th Computer Security Foundations Symposium, pp.114-128, 2011.
DOI : 10.1109/CSF.2011.15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.204.7197

A. Mciver and C. Morgan, Abstraction, Refinement And Proof For Probabilistic Systems, Monographs in Computer Science, 2004.

A. Miné, The octagon abstract domain. Higher-Order and Symbolic Computation, HOSC), vol.19, issue.1, pp.31-100, 2006.

D. Monniaux, Abstract Interpretation of Probabilistic Semantics, SAS '00, pp.322-339, 2000.
DOI : 10.1007/978-3-540-45099-3_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.97.818

G. Necula, S. Mcpeak, S. Rahul, and W. Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, CC '02, pp.213-228, 2002.
DOI : 10.1007/3-540-45937-5_16

A. Neumaier and O. Shcherbina, Safe bounds in linear and mixed-integer linear programming, Mathematical Programming, vol.99, issue.2, pp.283-296, 2004.
DOI : 10.1007/s10107-003-0433-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.373.508

R. Parikh, On Context-Free Languages, Journal of the ACM, vol.13, issue.4, pp.570-581, 1966.
DOI : 10.1145/321356.321364

S. Sankaranarayanan, A. Chakarov, and S. Gulwani, Static analysis for probabilistic programs: Inferring whole program properties from finitely many paths, PLDI '13, pp.447-458, 2013.
DOI : 10.1145/2499370.2462179

P. Suriana, Fourier-Motzkin with Non-Linear Symbolic Constant Coefficients, Massachusetts Institute of Technology, 2016.

P. Van-hentenryck, A. Cortesi, L. Charlier, and B. , Type analysis of prolog using type graphs, The Journal of Logic Programming, vol.22, issue.3, pp.179-209, 1995.
DOI : 10.1016/0743-1066(94)00021-W

A. Venet, Automatic analysis of pointer aliasing for untyped programs, Science of Computer Programming, vol.35, issue.2-3, pp.223-248, 1999.
DOI : 10.1016/S0167-6423(99)00012-X

S. Villemot, Automates finis et intérpretation abstraite: Application à l'analyse statique de protocoles de communication, 2002.