Maximal Quantified Precondition Synthesis for Linear Array Loops

Precondition inference is an important problem with many applications in verification and testing. Finding preconditions can be tricky as programs often have loops and arrays, which necessitates finding quantified inductive invariants. However, existing techniques have limitations in finding such invariants, especially when preconditions are missing. Further, maximal (or weakest) preconditions are often required to maximize the usefulness of preconditions. So the inferred inductive invariants have to be adequately weak. To address these challenges, we present an approach for maximal quantified precondition inference using an \emph{infer-check-weaken} framework. Preconditions and inductive invariants are inferred by a novel technique called \emph{range abduction}, and then checked for maximality and weakened if required. Range abduction attempts to propagate the given quantified postcondition backwards and strengthen or weaken it as needed to establish inductiveness. Weakening is done in a syntax-guided fashion. Our evaluation performed on a set of public benchmarks demonstrates that the technique significantly outperforms existing techniques in finding maximal preconditions and inductive invariants.