Craig Interpretation

Abstract. Abstract interpretation (AI) is one of the most scalable au-tomated approaches to program verification available today. To achieve efficiency, many steps of the analysis, e.g., joins and widening, lose pre-cision. As a result, AI often produces false alarms, coming from the inability to find a safe inductive invariant even when it exists in a chosen abstract domain. To tackle this problem, we present Vinta, an iterative algorithm that uses Craig interpolants to refine and guide AI away from false alarms. Vinta is based on a novel refinement strategy that capitalizes on recent advances in SMT and interpolation-based verification to (a) find coun-terexamples to justify alarms produced by AI, and (b) to strengthen an invariant to exclude alarms that cannot be justified. The refinement process continues until either a safe inductive invariant is computed, a counterexample is found, or resources are exhausted. This strategy allows Vinta to recover precision lost in many AI steps, and even to compute inductive invariants that are inexpressible in the chosen abstract domain (e.g., by adding disjunctions and new terms). We have implemented Vinta and compared it against top verification tools from the recent software verification competition. Our results show that Vinta outperforms state-of-the-art verification tools.