Microsoft Research
Microsoft Translator |
Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain

K. Rustan M. Leino and Francesco Logozzo
May 2007

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
Share
Share this page on Facebook
Share this page on Twitter
Share this page on LinkedIn
E-mail this page
RSS feeds
> Publications > Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain