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.

References in zbMATH (referenced in 12 articles )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
  2. Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano: Infinite-state invariant checking with IC3 and predicate abstraction (2016)
  3. Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
  4. Dragan, Ioan; Kovács, Laura: Lingva: generating and proving program properties using symbol elimination (2015)
  5. Sharma, Rahul; Gupta, Saurabh; Hariharan, Bharath; Aiken, Alex; Liang, Percy; Nori, Aditya V.: A data driven approach for algebraic loop invariants (2013)
  6. Amato, Gianluca; Parton, Maurizio; Scozzari, Francesca: Discovering invariants via simple component analysis (2012)
  7. Neider, Daniel: Computing minimal separating DFAs and regular invariants using SAT and SMT solvers (2012)
  8. Colón, Michael A.; Sankaranarayanan, Sriram: Generalizing the template polyhedral domain (2011)
  9. Gaudel, Marie-Claude: Checking models, proving programs, and testing systems (2011) ioport
  10. Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Rybalchenko, Andrey: Aligators for arrays (tool paper) (2010)
  11. Jung, Yungbum; Kong, Soonho; Wang, Bow-Yaw; Yi, Kwangkeun: Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction (2010)
  12. Gupta, Ashutosh; Rybalchenko, Andrey: InvGen: an efficient invariant generator (2009) ioport