Oasis: ILP-Guided Synthesis of Loop Invariants
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.
Cite
Text
Bhatia et al. "Oasis: ILP-Guided Synthesis of Loop Invariants." NeurIPS 2020 Workshops: CAP, 2020.Markdown
[Bhatia et al. "Oasis: ILP-Guided Synthesis of Loop Invariants." NeurIPS 2020 Workshops: CAP, 2020.](https://mlanthology.org/neuripsw/2020/bhatia2020neuripsw-oasis/)BibTeX
@inproceedings{bhatia2020neuripsw-oasis,
title = {{Oasis: ILP-Guided Synthesis of Loop Invariants}},
author = {Bhatia, Sahil and Padhi, Saswat and Natarajan, Nagarajan and Sharma, Rahul and Jain, Prateek},
booktitle = {NeurIPS 2020 Workshops: CAP},
year = {2020},
url = {https://mlanthology.org/neuripsw/2020/bhatia2020neuripsw-oasis/}
}