Abstract

Automated synthesis of inductive invariants is an important problem in software verification. We propose a novel technique that is able to solve complex loop invariant synthesis problems involving large number of variables. We reduce the problem of synthesizing invariants to a set of integer linear programming (ILP) problems. We instantiate our techniques in the tool Oasis that outperforms state-of-the-art systems on benchmarks from the invariant synthesis track of the Syntax Guided Synthesis competition.

BibTeX Citation

@article{cap_neurips20/bhatia/oasis,
  title         = {OASIS: ILP-Guided Synthesis of Loop Invariants},
  author        = {Sahil Bhatia and
                   Saswat Padhi and
                   Nagarajan Natarajan and
                   Rahul Sharma and
                   Prateek Jain},
  booktitle     = {Proceedings of the NeurIPS 2020 Workshop on Computer-Assisted Programming,
                   December 12, 2020},
  year          = {2020},
  url           = {https://openreview.net/pdf?id=T591RKxIh6Q}
}