Three complementary verification approaches exist for real-time concurrent programs: (i) Timed Automata (TA) model checkers reason rigorously about timing but cannot express C’s memory model and synchronization primitives. (ii) Program verifiers handle advanced language features but ignore timing, producing spurious errors when timing makes races impossible. (iii) Worst-Case Execution Time (WCET) analyzers bound execution time but cannot verify safety properties. We present a vision for timing-aware program verification and propose a workflow that integrates: (i) TA semantics, (ii) existing C program verifier capabilities, and (iii) WCET timing estimates. We identify three key research challenges and demonstrate feasibility through a prototype implementation in a state-of-the-art software model checker. Our prototype demonstrates the potential to eliminate false positives from timing-infeasible scenarios and verify real-time properties previously impossible to express in C program verifiers.