InvGen: An Efficient Invariant Generator

Abstract. 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.

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Ashutosh Gupta, Andrey Rybalchenko
• Keywords: Arithmetic Invariant Generator, CAV 2009, Formal Methods, Imperative Programs, Invariant Generation Order