Abstract: Recently, real-time verification tools such as UPPAAL, KRONOS and HyTech have been applied to synthesize feasible solutions to static scheduling problems. The basic common idea of these works is to reformulate the scheduling problem as a reachability problem that can be solved by the verification tools. The model of Linearly Priced Timed Automata extends the model of timed automata with prices on transitions and locations. This generalizes previous results on minimum-time reachability and accumulated delays in timed automata. A main difference between verification algorithms and dedicated scheduling algorithms is in the way they search the state-space. Scheduling algorithms are often designed to find optimal (or near optimal) solutions quickly. In contrast, verification algorithms do normally not support any notion of optimality. They are designed to explore the entire state-space as efficiently as possible. In order to reduce the gap between scheduling and verification algorithms, we adopt a number of techniques used in scheduling algorithms in the verification tool UPPAAL.