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.