In this thesis we introduce an abstraction refinement-based verification framework for concurrent systems. Our approach to abstraction is based on a combination of predicate abstraction, a data abstraction technique, and spotlight abstraction, a technique that abstracts away entire processes of a concurrent system. We thus tackle two major causes of state explosion in verification of concurrent systems. Another key feature of our approach is the use of a three-valued abstract domain. Properties in our system models can take the values true, false and unknown, which enables us to explicitly model the loss of information due to abstraction: All true and false results obtained via verification can be transferred to the original system, only unknown necessitates refinement. For refining the abstract models we follow the concept of counterexample-guided abstraction refinement (CEGAR). Counterexamples are unknown error paths in the model that typically hint at several possible ways to resolve the uncertainty via refinement. In our scenario, these refinement steps can involve the addition of new predicates or processes. However, not every potential refinement step is expedient, which makes the selection of an appropriate step exceedingly difficult. Therefore, we introduce an enhanced variant of CEGAR: Based on an abstraction dependence analysis the possible refinement steps, that we have derived from a counterexample, are heuristically evaluated with regard to their benefit for the current verification task, and the best evaluated step is chosen for refinement. We demonstrate that our heuristic approach can significantly improve the performance of abstraction-refinement-based verification. Our developed verification framework allows for reasoning about CTL properties of fixed-sized and parameterised concurrent systems.