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.

wing07.pdf
PDF file

In  International Workshop on Invariant Generation

Details

TypeInproceedings
InstitutionRISC, Hagenberg, Austria
> Publications > Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain