  We describe a system to prove properties of programs. The key feature of this
approach is a method to automatically synthesize inductive invariants of the
loops contained in the program. The method is generic, i.e., it applies to a
large set of programming languages and application domains; and lazy, in the
sense that it only generates invariants that allow one to derive the required
properties. It relies on an existing system called GPiD for abductive reasoning
modulo theories, and on the platform for program verification Why3. Experiments
show evidence of the practical relevance of our approach.
