The Project R1 advances the automatic verification of real-time systems that are described by of high-level specifications exhibiting the three dimensions of process behavior, complex infinite data, and continuous real-time. To this end, transformation and decomposition techniques are combined with proof procedures resting on the paradigms of abstraction refinement and local theory extensions.