InvGen

InvGen: An Efficient Invariant Generator. In this paper we present InvGen, an automatic linear arithmetic invariant generator for imperative programs. InvGen’s unique feature is in its use of dynamic analysis to make invariant generation order of magnitude more efficient.