Abstract interpretation serves as a powerful theoretical tool for developing and justifying program-analysis algorithms. It provides a way to establish that information extracted from a program by a program-analysis algorithm is a meaningful characterization of what can occur when the program is executed. Typically, however, it is not an easy task to obtain the appropriate abstract state-transformation functions and to show that they are correct. On the contrary, papers on program analysis often contain exhaustive (and exhausting) proofs to demonstrate that a given abstract semantics provides answers that are safe with respect to a given concrete semantics.