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, and lemmas on demand, as used in automatic theorem proving. In line with this trend, the author shows a technique that combines abstract interpretation 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 also includes a demo of the Spec# programming system, which makes use of loop-invariant inference, verification-condition generation, and automatic theorem proving to reason about object-oriented programs.
展开▼
