Behavior Approximation: Abstractions are also described in term of the relative behavior of the abstract system versus the concrete system. A program’s “behavior” is defined as the set of possible execution paths, also called traces or computations. These are the allowable sequences of program states, starting from a valid initial state. It includes:
- Over-approximation
- Under-approximation
- Exact Abstraction