Automatic Generation of Invariants in Processor Verification. - Jeffrey X. Su; David L. Dill; Clark W. Barrett (FMCAD, 1996)

Formally Verifying Data and Control with Weak Reachability Invariants. - Jeffrey X. Su; David L. Dill; Jens U. Skakkebæk (FMCAD, 1998)