InvGen: An Efficient Invariant Generator

  • Ashutosh Gupta
  • Andrey Rybalchenko
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


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.


Error Location Abstract Interpretation Program Variable Symbolic Execution Invariant Generation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proc. PLDI, pp. 300–309. ACM Press, New York (2007)Google Scholar
  2. 2.
    Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science. AMS (1967)Google Scholar
  4. 4.
    Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262–276. Springer, Heidelberg (2009)Google Scholar
  5. 5.
    Gupta, A., Rybalchenko, A.: InvGen: an efficient invariant generator,
  6. 6.
    Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL 2004: Principles of Programming Languages, pp. 232–244. ACM, New York (2004)Google Scholar
  7. 7.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of ACM (1969)Google Scholar
  8. 8.
    Ku, K., Hart, T., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: Proc. ASE (2007)Google Scholar
  9. 9.
    Lalire, G., Argoud, M., Jeannet, B.: The interproc analyze,
  10. 10.
    Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Ashutosh Gupta
    • 1
  • Andrey Rybalchenko
    • 1
  1. 1.Max Planck Institute for Software Systems (MPI-SWS)Germany

Personalised recommendations