Timed automata are a popular model for verification of real-time systems. Algorithms for their analysis form the core of several industry-strength software. Most of these algorithms work only for a special class of timed automata where so-called diagonal constraints are absent. However, diagonal constraints are a convenient feature for modeling, and using them judiciously can result in much smaller models. The goal of this thesis is to develop efficient algorithms in the setting of diagonal constraints and investigate their scalability on industrial examples provided by Tata Research Development and Design Centre (Pune, India).