Efficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill. However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables. This paper reports on work attacking these explosion problems by developing and combining {\sl compositional} and {\sl symbolic} model-checking techniques. The presented techniques provide the foundation for a new automatic verification tool UPPAAL. Experimental results show that UPPAAL is not only substantially faster than other real-time verification tools but also able to handle much larger systems.