Abstract interpretation is one of the main verification technologies
besides model checking and deductive verification.
Model checking and abstract interpretation both compute properties
of programs or other systems by fixpoint iteration.
We explain abstract interpretation using examples from a particular
application domain, the determination of bounds on the execution
times of programs.These bounds are used to show reliably that
hard real-time systems satisfy their timing constraints.
The application domain is rich enough to offer a wealth of static analyses.
Some are obtained as Galois connections from the collecting semantics,
other that cannot be obtained by Galois connections,
some that satisfy the ascending chain condition and others that require
widening because their domains possess infinite ascending chains.
Run-time guarantees play an important role in the area of embedded
systems and especially hard real-time systems. These bounds must
be safe, i.e., they may never underestimate the real execution time.
Furthermore, they should be tight, i.e., the overestimation should be as
small as possible.
In modern microprocessor architectures, caches, pipelines, and all kinds
of speculation are key features for improving (average-case) performance.
Unfortunately, they make the analysis of the timing behaviour of instructions
very difficult, since the execution time of an instruction depends on the
execution history.