A major challenge in software verification is choosing a suitable abstraction which yields a tractable yet still precise enough program model. However, automatically picking a suitable abstraction requires nontrivial insights and is usually implemented using heuristics. Though heuristics determine the efficiency of most verification tools, they are typically not formally described and hardcoded in the source code of tools. Furthermore, heuristics tight a verification tool to a restricted application domain. This causes another verification challenge  an optimal choice of a verifcation tool for a given task. We conjecture that the two challenges, namely automatically choosing programspecific abstraction and automatically picking an optimal tool for a verification task, can be solved by identifying in a program typical patterns of variable use. Examples of these patterns are bitvectors, counters, loop iterators, and so on. We formalise and study the concept of a variable role, which captures the implicit knowledge about these patterns. We identify most frequent variable roles in practical open source programs and define a framework for a formal specification of variable roles using Datalog. We explore the application of variable roles in software verification in two settings. First, we create a portfolio solver which chooses a tool for a given verification task, using variablerolebased program metrics. We evaluate our portfolio solver in the setting of the software verification competition SVCOMP. Second, we define a framework to systematically specify variablerolebased heuristics to automatically generate program abstraction. We integrate our method in the model checker Eldarica to generate predicates for initial abstraction and to guide abstraction refinement through templates provided for Craig interpolation. We evaluate our approach on a subset of benchmarks from SVCOMP and verification benchmarks from the literature.
