Domain types: Abstract-domain selection based on variable usage

Abstract. The success of software model checking depends on finding an ap-propriate abstraction of the program to verify. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be fa-miliar with the tradeoffs and performance details of the available abstract do-mains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types (e.g., ‘int ’ and ‘long’) to guide the selection of an appropriate abstract domain for a model checker. Our implementation on top of an existing verification framework determines the domain type for each variable in a pre-analysis step, based on the domain. Based on a series of experiments on a comprehensive set of verification tasks from international verification competitions, we demonstrate that the choice of the abstract domain per variable (we consider one explicit and one symbolic domain) can substantially improve the verification in terms of performance and precision.