Over-approximation: Over-approximation occurs when there are more behaviors in the abstract system than the concrete system. This approach provides a popular class of weakly preserving abstractions for properties that hold on all paths of a program (e.g., safety properties or more general universally quantified path properties such as LTL). Weak preservation holds because when behaviors (execution paths) are added to create the abstract system, any property that is true for all paths is true for any subset of those paths—including the subset that exactly describes the behavior of the concrete system. However, due to over-approximation, errors that are reported for the behaviors of the abstract program may not correspond to behaviors in the original program. To enable verification, these “spurious” errors must be removed by reducing the degree of over-approximation. The goal is to find an abstraction that is precise enough to allow verification of a property, while abstract enough to make verification practically tractable.