On Scaling Data-Driven Loop Invariant Inference

Sahil Bhatia, Saswat Padhi, Nagarajan Natarajan +2

Automated synthesis of inductive invariants is an important problem in software verification. Once all the invariants have been specified, software verification reduces to checking…