Derived variables
•Successfully produces desired invariants
•Adds many new variables
–slowdown
–irrelevant invariants
•Staged derivation and invariant inference
–avoid deriving meaningless values
–avoid computing tautological invariants
[Don’t say “false positive”; it has a technical meaning and people won’t know whether the false positive is regarding truth or relevance.]

The solution to “slowdown” is here on this slide.
The solution to “irrelevant invariants” will come soon.