Cyber-physical systems (CPS) are pervasively embedded into our lives and increasingly act in close proximity to as well as with direct impact on humans. Because of their safety-criticality, formal verification techniques that guarantee correctness properties for all of the infinitely many possible states of a CPS are of paramount importance. Since formal verification of CPS is known to be undecidable for realistic models, techniques to handle system complexity are needed. Verification methods based on hybrid automata focus on full automation and are therefore restricted to less expressive classes of CPS, while deductive verification methods rely on human guidance to make progress despite undecidability. To make human guidance possible, however, the inherent complexities of CPS practically mandate techniques to handle system complexity. This thesis introduces a component-based verification approach for CPS based on deductive verification. ^Crucially, the approach builds safety proofs about systems from smaller component proofs without analyzing the systems as a whole. As a result, the approach reduces verification complexity while simultaneously increasing proof reusability and maintainability. We develop the approach in three stages of increasing generality and suitable to various areas of application. First, we focus on modeling and verification of large traffic networks, and aim at avoiding traffic breakdowns on roads (i.e., the number of cars must not exceed the road's capacity) as fixed safety property. Second, we generalize flow exchange between components to instantaneous, lossless information exchange being restricted to globally known regions (e.g., robot position relative to a fixed reference point) and allow arbitrary safety properties. ^Third, we relate component time to global system time in order to describe information exchange history in terms of the magnitude of change and rate of change (e.g., robot position relative to previous position some time ago). We show the applicability of these three approaches by modeling examples from traffic control, vehicle control and autonomous robots. The results indicate that, compared to monolithic analysis, our approaches reduce verification effort, increase proof automation, facilitate reuse of component proofs and increase the overall maintainability of a verified CPS.