On Scaling Data-Driven Loop Invariant Inference

TL;DR

This paper presents a scalable data-driven approach for automatic inference of inductive invariants in software verification, addressing previous limitations in handling programs with many variables.

Contribution

The authors introduce the oasis tool, which enhances the scalability of data-driven invariant inference and outperforms existing systems on benchmark problems.

Findings

Oasis significantly improves scalability over prior data-driven invariant inference methods.

Oasis outperforms state-of-the-art systems on benchmark problems.

The approach effectively handles programs with a larger number of variables.

Abstract

Automated synthesis of inductive invariants is an important problem in software verification. Once all the invariants have been specified, software verification reduces to checking of verification conditions. Although static analyses to infer invariants have been studied for over forty years, recent years have seen a flurry of data-driven invariant inference techniques which guess invariants from examples instead of analyzing program text. However, these techniques have been demonstrated to scale only to programs with a small number of variables. In this paper, we study these scalability issues and address them in our tool oasis that improves the scale of data-driven invariant inference and outperforms state-of-the-art systems on benchmarks from the invariant inference track of the Syntax Guided Synthesis competition.