Incompleteness, counterexamples and refinements in abstract model-checking