Share this page
Share this page E-mail this page Print this page RSS feeds
Home > 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

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

Type: Inproceedings
Institution: RISC, Hagenberg, Austria