Time stamps were introduced in Shivers's PhD thesis for approximating the result of a control-flow analysis. We show them to be suitable for computing program analyses where the space of results (e.g., control-flow graphs) is large. We formalize time-stamping as a top-down, fixed-point approximation algorithm which maintains a single copy of intermediate results. We then prove the correctness of this algorithm.
Seventeenth Conference on the Mathematical Foundations of Programming Semantics: Electronic Notes in Theoretical Computer Science, 2001, p. 65-76