Using Widenings to Infer Loop Invariants Inside an SMT Solver, Or: A Theorem Prover As Abstract Domain

This paper presents a new technique for combining the inference power of abstract interpretation with the precision and flexibility of an automatic satisfiability modulo theories theorem prover.