"SMT-AI: an Abstract Interpreter as Oracle for k-induction."

Pierre Roux, Remi Delmas, Pierre-Loïc Garoche (2010)
a service of  Schloss Dagstuhl - Leibniz Center for Informatics