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

The last decade has seen a major development of verification techniques based on SMT solvers used to prove inductive invariants on systems. This approach allows to prove functional properties and scale up to handle industrial problems. However, it often needs a man in the loop to provide hand-written lemmas on the system in order to help the analysis and complete the proof.This paper presents a tool that automatically generates lemmas. It takes such systems and over-approximates their collecting semantics, providing a bound on the numerical memories. It is based on the abstract interpretation methodology introduced by Cousot in 1977.