Terminology and Concepts of our CFG based program representation

Program state

• Q: What is a state of a program?
• A: A map that assigns each variable a value. (Alternative terminology: call this map a valuation and say that a state is a pair of a location and a valuation. In fact for programs with several procedures the first component is not a location but a stack of locations, for multithreaded programs the first component is a list of locations, and for multithreaded programs with procedure calls it would be a list of stacks of locations.)

Sets of program states

• Q: How do we represent a set of program states?
• A: We use a formula whose free variables are the program variables. Each satisfying assignment is a state.

Control flow graph

A control flow graph (CFG) is a graph whose nodes we call locations and whose edges are labelled with statements. It is probably easy to imagine how a CFG for a given program looks like. An example can be seen on the Ultimate Automizer SV-COMP 2014 poster. A formal definition of a CFG for a program would be quite large, since this would require a formal definition of the underlying programming language. In our representation, the edges of a CFG are not labelled with program statements but with binary relations that define the effect of a statement.

Transition relations

• Q: How do we represent a transition relation?
• A: Conceptually, we use a formula over primed and unprimed program variables. The unprimed variables represent the value before executing the transition, the primed variables represent the values after executing the transition. E.g., if we want to state that the variable x was incremented by one and that the variable y was not changed, we use the formula x' = x+1 /\ y' = y. In our implementation, we use the TransFormula class to represent binary transition relations over primed and unprimed variables.