P. A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay, General decidability theorems for infinite-state systems, LICS, 1996.

A. R. Bradley, Sat-based model checking without unrolling, pp.70-87, 2011.

K. L. Mcmillan, Lazy abstraction with interpolants, CAV, pp.123-126, 2006.

A. Mebsout, Inférence d'invariants pour le model checking de systèmes paramétrés, 2014.

S. Conchon, A. Goel, S. Krsti´ckrsti´c, A. Mebsout, and F. Zaïdi, Cubicle: A Parallel SMT-Based Model Checker for Parameterized SystemsTool Paper, CAV, pp.718-724, 2012.

, Invariants for finite instances and beyond, FMCAD, pp.61-68, 2013.

S. Ghilardi and S. Ranise, Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis, LMCS, vol.6, issue.4, 2010.

S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Towards SMT model checking of array-based systems, Automated Reasoning, 4th International Joint Conference, pp.67-82, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00576600

K. L. Mcmillan, Lazy annotation revisited, Computer Aided Verification-26th International Conference, pp.243-259, 2014.

A. Cimatti, A. Griggio, S. Mover, and S. Tonetta, Infinite-state invariant checking with IC3 and predicate abstraction, Formal Methods in System Design, vol.49, issue.3, pp.190-218, 2016.

K. Hoder and N. Bjørner, Generalized property directed reachability, Theory and Applications of Satisfiability Testing-SAT 2012-15th International Conference, pp.157-171, 2012.

K. Hoder, N. Bjørner, and L. M. De-moura, µZ-an efficient engine for fixed points with constraints, Computer Aided Verification23rd International Conference, pp.457-462, 2011.