In hard real-time systems, operations are subject to timing constraints, i.e. there are operational deadlines from events to system responses. To show the correctness of such systems, one must therefore derive guarantees on the timeliness of reactions. Thereby, one fundamental problem is to characterize the execution time of programs. The execution time of a program depends on the program's input as well as on the underlying hardware architecture. Modern microprocessors feature many components that speed up computation by speculation, e.g. branch predictors, caches, and pipelines.