On Scaling Data-Driven Loop Invariant Inference
This addresses the problem of scaling automated software verification for developers, though it appears incremental as it builds on existing data-driven methods.
The paper tackled the scalability limitations of data-driven loop invariant inference techniques, which previously only worked on programs with few variables, by developing the tool oasis that outperforms state-of-the-art systems on benchmarks from the Syntax Guided Synthesis competition.
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.