the increment operation, that is, $0$ and $\mathbb{Z}_{\leq 0}$. This simplification of an abstract domain relatively to a semantic function is formalized in the most general abstract interpretation setting. This allows us to provide, for generic continuous semantic functions, a systematic and constructive method, that we call *correctness kernel*, for simplifying a given abstraction $A$ relatively to a given semantic function $f$ towards the unique minimal abstract domain that induces an equivalent approximate behavior of $f$ as in $A$. We show how correctness kernels can be embedded within the CEGAR methodology by providing a novel refinement heuristics in a CEGAR iteration step which turns out to be more accurate than the basic refinement heuristics [@cgjlv03]. We also describe how correctness kernels may be applied in predicate abstraction-based model checking [@ddp99; @gs97] for reducing the search space without applying Ball et al.’s [@bpr03] Cartesian abstractions, which typically yield additional loss of precision.

This is an extended and revised version of the conference paper [@gr10] that includes full proofs.

Correctness Kernels
===================

As usual in standard abstract interpretation [@CC77; @CC79], abstract domains (or abstractions) are specified by Galois connections/insertions (GCs/GIs for short) or, equivalently, adjunctions. Concrete and abstract domains, $\tuple{C,\leq_C}$ and $\tuple{A,\leq_A}$, 