# Abstract Interpretation Recipe

## Program Representation

Control-flow graph: where

- is set of program points
- are control-flow graph edges
- , so each is relation describing the meaning of command between and

We can define meaning of program in this form using collecting semantics.

## Summary of key steps

- design abstract domain that represents sets of program states
- define giving meaning to elements of
- define lattice ordering on such that
- define that maps an abstract element and a CFG statement to new abstract element, such that

(for example, by defining function so that becomes a Galois Connection and letting )

- extend to work on control-flow graphs, by defining as follows (below, )

which is analogous to collecting semantics.

(Note the Equivalent Form of Abstract Interpretation Function.)

- compute (this is easier than computing collecting semantics because lattice is simpler than ):

where for all .