Running

i = 0;
while (i < 5) {
  i = i + 1;
}

Running Collatz example

A path through graph

A trace for a given path: add states of variables

An execution trace through control-flow graph

One way: by deterministic execution, store the states

Example

Another way: updating set of reachable states until they stabilize

This is useful if we have non-determinism

• unknown inputs
• like NDFA

Analysis is similar to execution

• when analyzing, we will not know exact values of variables
• we wish to check for all possible initial state of e.g. procedure

This is called “collecting semantics”

Equations for collecting semantics

• recall one step operational semantics
• here we have semantics for basic commands
• they are then propagated through the graph