In plain words: A tool guesses loop invariants from example values instead of reading program text, and is built to handle programs with many variables. On standard invariant-inference benchmarks it beat the best existing tools.
Abstract · On Scaling Data-Driven Loop Invariant Inference
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.
Sahil Bhatia, Saswat Padhi, Nagarajan Natarajan, Rahul Sharma, Prateek Jain
arXiv:1911.11728 · cs.LG, cs.PL, cs.SE, stat.ML · submitted Nov 26, 2019 · updated Jul 16, 2020
abstract · pdf · html