Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain

K. Rustan M. Leino and Francesco Logozzo

Abstract

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.

Details

Publication typeInproceedings
Published inInternational Workshop on Invariant Generation
InstitutionRISC, Hagenberg, Austria
> Publications > Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain