This paper presents a method for using timing assumptions to prove automatically that an implementation meets a speed-independent specification. The method uses delay information in state-graph verification of finite-state concurrent systems. Timing assumptions are given as constant upper and lower bounds on delays between events. The approach is based on a continuous model of time, where times are real numbers. The method extends speed-independent methods based on finite automata on infinite sequences, allowing it to handle liveness properties and indeterminate computations. A formal framework is constructed to prove the soundness and completeness of the method. The fundamental idea is to associate each state with a convex linear region describing the states of individual timers, which are fictitious components that track possible event times. This automaton can eliminate computation sequences that violate timing assumptions. The cost of the method is a single exponential in the number of timers and the size of the specification automaton. The paper discusses three major categories of timing models: discrete time models, continuous time models with a global clock, and integer-bounded continuous time models. The first category assumes time is isomorphic to integers, while the second uses a global clock for timing assertions. The third model allows for more flexible coupling between system events and timing. The paper presents a framework for speed-independent verification, using trace sets to represent possible system histories. A trace set is a set of infinite sequences of events. The framework is similar to other trace models of concurrency and linear temporal logic (LTL), with the primary difference being that LTL formulas do not have explicit alphabets. The paper then discusses the use of timers in timing constraints. Timers are fictitious "alarm clocks" that can be set to arbitrary real values within specified bounds. The method uses a timer region automaton to enforce ordering constraints between timer events based on user-supplied delay bounds. The automaton is the conjunction of a well-formedness automaton and a timer region automaton. The paper also discusses the representation of timer regions using difference bound matrices (DBMs). DBMs are used to represent bounds on individual timer values and the differences between timer values. The paper shows that DBMs can be used to represent timer regions uniquely and efficiently. The paper concludes with a proof of the convergence lemma, which shows that the number of regions in the timer region automaton is finite. This is important because it ensures that the automaton can be used for verification. The paper also discusses the use of DBMs in the transition function of the timer region automaton, showing how the effects of timer events can be modeled.This paper presents a method for using timing assumptions to prove automatically that an implementation meets a speed-independent specification. The method uses delay information in state-graph verification of finite-state concurrent systems. Timing assumptions are given as constant upper and lower bounds on delays between events. The approach is based on a continuous model of time, where times are real numbers. The method extends speed-independent methods based on finite automata on infinite sequences, allowing it to handle liveness properties and indeterminate computations. A formal framework is constructed to prove the soundness and completeness of the method. The fundamental idea is to associate each state with a convex linear region describing the states of individual timers, which are fictitious components that track possible event times. This automaton can eliminate computation sequences that violate timing assumptions. The cost of the method is a single exponential in the number of timers and the size of the specification automaton. The paper discusses three major categories of timing models: discrete time models, continuous time models with a global clock, and integer-bounded continuous time models. The first category assumes time is isomorphic to integers, while the second uses a global clock for timing assertions. The third model allows for more flexible coupling between system events and timing. The paper presents a framework for speed-independent verification, using trace sets to represent possible system histories. A trace set is a set of infinite sequences of events. The framework is similar to other trace models of concurrency and linear temporal logic (LTL), with the primary difference being that LTL formulas do not have explicit alphabets. The paper then discusses the use of timers in timing constraints. Timers are fictitious "alarm clocks" that can be set to arbitrary real values within specified bounds. The method uses a timer region automaton to enforce ordering constraints between timer events based on user-supplied delay bounds. The automaton is the conjunction of a well-formedness automaton and a timer region automaton. The paper also discusses the representation of timer regions using difference bound matrices (DBMs). DBMs are used to represent bounds on individual timer values and the differences between timer values. The paper shows that DBMs can be used to represent timer regions uniquely and efficiently. The paper concludes with a proof of the convergence lemma, which shows that the number of regions in the timer region automaton is finite. This is important because it ensures that the automaton can be used for verification. The paper also discusses the use of DBMs in the transition function of the timer region automaton, showing how the effects of timer events can be modeled.