R. Carl-backhouse, Galois Connections and Fixed Point Calculus, Lecture Notes in Computer Science, vol.2297, pp.89-148, 2000.
DOI : 10.1007/3-540-47797-7_4

F. Besson, T. P. Jensen, D. Pichardie, and T. Turpin, Certified Result Checking for Polyhedral Analysis of Bytecode Programs
DOI : 10.1007/978-3-642-15640-3_17
URL : https://hal.archives-ouvertes.fr/inria-00537816

M. Colón, S. Sankaranarayanan, and H. Sipma, Linear Invariant Generation Using Non-linear Constraint Solving, Lecture Notes in Computer Science, vol.2725, pp.420-432, 2003.
DOI : 10.1007/978-3-540-45069-6_39

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

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-96, 1978.
DOI : 10.1145/512760.512770

D. Cox, J. Little, and D. O. Shea, Ideals, varieties, and algorithms . Undergraduate Texts in Mathematics An introduction to computational algebraic geometry and commutative al- gebra, 2007.

J. Faugère, A new efficient algorithm for computing Gröbner bases without reduction to zero (F5), ISSAC, pp.75-83, 2002.

M. Karr, Affine relationships among variables of a program, Acta Informatica, vol.6, issue.2, pp.133-151, 1976.
DOI : 10.1007/BF00268497

L. Kovács, A Complete Invariant Generation Approach for P-solvable Loops, Ershov Memorial Conference, pp.242-256, 2009.
DOI : 10.1007/978-3-642-11486-1_21

Z. Manna, Mathematical Theory of Computation, 1974.

M. Müller-olm and H. Seidl, Polynomial Constants Are Decidable, SAS, pp.4-19, 2002.
DOI : 10.1007/3-540-45789-5_4

M. Müller-olm and H. Seidl, Computing polynomial program invariants, Information Processing Letters, vol.91, issue.5, pp.233-244, 2004.
DOI : 10.1016/j.ipl.2004.05.004

E. Rodríguez-carbonell and D. Kapur, An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants, Lecture Notes in Computer Science, vol.3148, pp.280-295, 2004.
DOI : 10.1007/978-3-540-27864-1_21

E. Rodríguez-carbonell and D. Kapur, Automatic generation of polynomial loop invariants: algebraic foundations, ISSAC, pp.266-273, 2004.

E. Rodríguez-carbonell and D. Kapur, Program Verification Using Automatic Generation of Invariants,, ICTAC, pp.325-340, 2004.
DOI : 10.1007/978-3-540-31862-0_24

E. Rodríguez-carbonell and D. Kapur, Automatic generation of polynomial invariants of bounded degree using abstract interpretation, Science of Computer Programming, vol.64, issue.1, pp.54-75, 2007.
DOI : 10.1016/j.scico.2006.03.003

E. Rodríguez-carbonell and D. Kapur, Generating all polynomial invariants in simple loops, Journal of Symbolic Computation, vol.42, issue.4, pp.443-476, 2007.
DOI : 10.1016/j.jsc.2007.01.002

S. Sankaranarayanan, H. B. Sipma, and Z. Manna, Constraint-Based Linear-Relations Analysis, Lecture Notes in Computer Science, vol.3148, pp.53-68, 2004.
DOI : 10.1007/978-3-540-27864-1_7

S. Sankaranarayanan, H. B. Sipma, and Z. Manna, Non-linear loop invariant generation using Gröbner bases, POPL, pp.318-329

G. Winskel, The Formal Semantics of Programming Languages, pp.12-15, 1993.