ompact abstractions for processor pipelines∗ Sebastian Hahn, Jan Reineke Informatik, Saarland University Saarbr¨ucken Reinhard Wilhelm Informatik, Saarland University and AbsInt Angewandte Informatik GmbH Saarbr¨ucken Hard real-time systems require programs to react on time. Static timing analysis derives timing guarantees by analyzing the behavior of programs on the underlying execution platform. Efficient abstractions have been found for the analysis of caches. Unfortunately, this is not the case for the analysis of processor pipelines. Pipeline analysis typically uses an expensive powerset domain of concrete pipeline states. Therefore, pipeline analysis is the most complex part of timing analysis. We propose a compact domain for pipeline analysis. This pipeline analysis determines the minimal progress of instructions in the program through the pipeline. We give a concrete semantics for an in-order pipeline, which forms the r an abstract semantics. On the way, we found out that ...