A trace of a program execution is the sequence of transitions of the program state:

Errorneous states are just states that satisfy some property $P$:

Testing may verify some traces if an error occurs:

But checking all possible programs are impossible:

Abstract interpretation approximates the concrete states with a less precise approximation:

Since it’s an over-approximation, it may falsely identify safe states as errorneous:

And additionally take into account states which would not actually be computed:

But it is a sound approximation, meaning it never not takes a concrete state into account:

And all concrete errorneous states must be correctly abstracted into an errorneous abstract state: