Almost all static analyses are overapproximating (safety) analyses, which overestimate a program's behavior in exchange for a guarantee of termination.

Overapproximating analyses can be defined in terms of Galois connections, that is, a pair of functions, $\alpha, \gamma$, where $\alpha$ defines how to map an input test-data set into an abstract value for static analysis, and $\gamma$ shows how to map the result of the analysis back to the overestimated set of outputs.

Underapproximating (liveness) analyses have gained in importance, and it is natural to try to dualize the Galois connection format, but the obvious dualization generates analyses that calculate no useful information.

This talk reviews overapproximation analysis, examines the underapproximation problem, and shows how the Galois connection framework can be applied to calculate both over- and underapproximations by using lower and upper powerdomain constructors, respectively, to construct the relevant abstract domains. Dennis Dams's under- and overapproximation analyses of state-transition systems for model checking are used as a case study.

If time allows, the role of logical relations in lifting the Galois connections to higher type and powerset type will be explained.