The development of time-critical systems (e.g., aircraft control systems or autonomous vehicles) require rigorous methods for guaranteeing the correct behavior of the system. Quite often, some characteristics of the system are unknown at design phase, and hence the need for introducing parameters specifying possible range of values in which the system must operate. This project aims at providing sound and efficient techniques for the verification of time-critical systems with parameters. We will consider a broad class of distributed real-time systems that can be specified as a real-time rewrite theories, where besides the usual features available for formalisms such as parametric timed automata (clocks, timed transitions, parameters, etc), it is also possible to consider unbounded data structures, user-defined data types, different forms of communications, and dynamic object creation and deletion. Such rewrite theories are also expressive enough to serve as a semantic framework for different industrial modeling languages; rewrite-based tools can then provide formal analysis methods to such languages. This project will contribute with: symbolic reachability methods for broad classes of real-time (rewrite) systems; sound and complete untimed and timed temporal logic model checking procedures; and a novel timed strategy language, allowing us to analyze a system whose executions are controlled by a user-defined strategy. We thus expect to extend significantly the analysis methods available for real-time systems.