In this paper we study the relation between the lack of completeness
in abstract interpretation of model-checking and the structure of the
counterexamples produced by the model-checker. We consider two dual
forms of completeness of an abstract interpretation: Forward and
backward completeness. They correspond respectively to the standard
$\gamma$/$\alpha$ completeness of an abstract interpretation and
can be related with each other by adjunction. We give a constructive
characterization of Clarke et al.'s spurious counterexamples in terms
of both forward and backward completeness of the underlying abstract
interpretation. This result allows us to understand the structure of
the counterexamples that can be removed by systematically refining
abstract domains to achieve completeness with respect to a given
operation. We apply our result to improve static program analysis
by refining the model-checking of an abstract interpretation.