Goal: Recover invariants
•Detect invariants such as those found in assert statements or specifications
–x > abs(y)
–x = 16*y + 4*z + 3
–array a contains no duplicates
–for each node n, n = n.child.parent
–graph g is acyclic
–…
Say “at a program point.”
…or in formal specifications.

(The last three are not all that likely in an assert statement…)

Segue:  why would we want to find them?  Now I will motivate that.