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 on Lattices)

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

which is analogous to Collecting Semantics

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

where for all