> Publications > Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain
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.
 PDF file |
In: International Workshop on Invariant Generation
Details
| Type: | Inproceedings |
| Institution: | RISC, Hagenberg, Austria |
Related People
©2009 Microsoft Corporation. All rights reserved.