View article

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.