# Transition System and Collecting Semantics - program counter values. Denoted (program point) or (vertex in CFG) - values of other variables

Transition system semantics:

• state is set of pairs • element of concrete lattice is a set of such pairs , i.e. • post maps set of such pairs to an extended set of such pairs, ## Collecting Semantics

Take . Because is an arbitrary set, for a given , there can be any number of such that is in (in fact, is a relation on ).

We can equivalently represent this relation as the following multi-valued function, by grouping all for a given :   Collecting semantics simply works with instead of , which is just notational change.

• lattice element is a function i.e. • we have function that transforms such functions and directly corresponds to 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 Compute the big relation on global states in terms of and . Then derive a nice expression for where . Now we come back to the definition of post, which was so we obtain Now instead of , consider , and define a new sp on such different representation. Then where We also represent as , then we obtain function that corresponds to :  Note that will be except at the entry into our control-flow graph.

If we compute , we obtain such that gives precisely the set of all reachable states at a program point . Such is isomorphic to .

We call this way of defining the collecting semantics of the program, because it collects all states for each program point. It will be convenient to define how abstract interpretation works.