Formal Program running time verification is an important issue in system design required for performance optimization under "first-time-right" design constraints and for real-time system verification. Simulation based approaches or simple instruction counting are not appropriate and risky for more complex architectures in particular with data dependent execution paths. Formal analysis techniques have suffered from loose timing bounds leading to significant performance penalties when strictly adhered to. We present an approach which combines simulation and formal techniques in a safe way to improve analysis precision and tighten the timing bounds. Using a set of processor parameters, it is adaptable to arbitrary processor architectures. The results show an unprecedented analysis precision allowing to reduce performance overhead for provably correct system or interface timing.