- English only

# Lab for Automated Reasoning and Analysis LARA

## Describing Reachable States using Collecting Semantics

**Main question:** What values can variables of the program take at different program points?

We can represent programs by control-flow graphs (CFG).

**Definition:** Control flow-graph is a graph with nodes , edges and for each edge a command given by relation , with initial and final node

Program points are CFG nodes. Statements are labels on CFG edges.

We look at a particular way of representing and computing sets of reachable states, splitting states by program counter (control-flow graph node): **collecting semantics**.

- states describing values of program variables (not including program counter).

For each program point , we have the set of reachable states .

The set of all reachable states of the program is .

Let be initial program counter and the set of values of program variables in .

The set of reachable states is defined as the least solution of constraints:

over variables for all of finitely many program points .

The last condition is equivalent to

Here is the relation giving semantics for the command associated with edge .

Set of recursive inequations in the lattice of products of sets. Note is equivalent to , so we have equations in lattice.

They specify function from pairs of sets of states to pairs of sets of states which is -morphism (and therefore monotonic).

Least fixpoint of is .

**Example**

Sets of states at selected points:

i = 20; x = 2; while (i > 0) { x = x + 4; i = i - 1; } if (x==0) { error; } else { y = 1000/x; }

After the assignment of to 2, the set of reachable states is