The last decade has displayed a trend for automatic reasoning techniques to operate on demand. Examples of this trend are counterexample-driven predicate refinement, as used in software model checking [7, 1, 8], and lemmas on demand, as used in automatic theorem proving [6, 5, 3, 0, 9]. In line with this trend, I will in this talk show a technique that combines abstract interpretation [4] and theorem proving, inferring program invariants when the theorem prover cannot proceed without them. This is joint work with Francesco Logozzo.

To motivate the technique, the talk will also include a demo of the Spec# programming system [2, 10], which makes use of loop-invariant inference, verificationcondition generation, and automatic theorem proving to reason about object-oriented programs.