Invgen: An efficient invariant generator
A Gupta, A Rybalchenko - … Conference, CAV 2009, Grenoble, France, June …, 2009 - Springer
A Gupta, A Rybalchenko
Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble …, 2009•SpringerInvGen: An Efficient Invariant Generator Page 1 InvGen: An Efficient Invariant Generator
Ashutosh Gupta and Andrey Rybalchenko Max Planck Institute for Software Systems (MPI-SWS)
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. 1 Introduction Program verification relies on
invariants for reasoning about sets of reachable states [3]. Synthesizing invariants that satisfy a …
Ashutosh Gupta and Andrey Rybalchenko Max Planck Institute for Software Systems (MPI-SWS)
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. 1 Introduction Program verification relies on
invariants for reasoning about sets of reachable states [3]. Synthesizing invariants that satisfy a …
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.
Springer
