  The success of software model checking depends on finding an appropriate
abstraction of the subject program. The choice of the abstract domain and the
analysis configuration is currently left to the user, who may not be familiar
with the tradeoffs and performance details of the available abstract domains.
We introduce the concept of domain types, which classify the program variables
into types that are more fine-grained than standard declared types, such as int
or long, in order to guide the selection of an appropriate abstract domain for
a model checker. Our implementation determines the domain type for each
variable in a pre-processing step, based on the variable usage in the program,
and then assigns each variable to an abstract domain. The model-checking
framework that we use supports to specify a separate analysis precision for
each abstract domain, such that we can freely configure the analysis. We
experimentally demonstrate a significant impact of the choice of the abstract
domain per variable. We consider one explicit (hash tables for integer values)
and one symbolic (binary decision diagrams) domain. The experiments are based
on standard verification tasks that are taken from recent competitions on
software verification. Each abstract domain has unique advantages in
representing the state space of variables of a certain domain type. Our
experiments show that software model checkers can be improved with a
domain-type guided combination of abstract domains.
