General decidability theorems for infinite-state systems, LICS, 1996. ,
Sat-based model checking without unrolling, pp.70-87, 2011. ,
Lazy abstraction with interpolants, CAV, pp.123-126, 2006. ,
Inférence d'invariants pour le model checking de systèmes paramétrés, 2014. ,
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.
Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis, LMCS, vol.6, issue.4, 2010. ,
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
Lazy annotation revisited, Computer Aided Verification-26th International Conference, pp.243-259, 2014. ,
Infinite-state invariant checking with IC3 and predicate abstraction, Formal Methods in System Design, vol.49, issue.3, pp.190-218, 2016. ,
Generalized property directed reachability, Theory and Applications of Satisfiability Testing-SAT 2012-15th International Conference, pp.157-171, 2012. ,
µZ-an efficient engine for fixed points with constraints, Computer Aided Verification23rd International Conference, pp.457-462, 2011. ,