There are many state-of-the-art techniques for loop bound analysis. Most of them target an upper bound for a given program, and others find a lower bound. Exact bound analysis still remains largely unexplored, but it offers new applications. To compute an exact bound for a program it is necessary to reason about the possible values the program’s inputs can take and how they relate to each other. Since inputs can vary on any given execution of the program, it makes the problem of computing an exact bound challenging. In this work, we present a new approach to find an exact bound by way of precondition synthesis which iteratively considers under-approximations of a program under which the bound can be precomputed over initial values of program variables. For each precondition, our approach synthesizes a function over program variables such that when the function is applied to the initial values of the program variables, its output is an exact bound for the program. We reduce the precondition synthesis problem to that of safety verification which lends its correctness guarantees to the exact bounds we compute. Our technique has been implemented in a tool called ELBA, and we show that it is effective on a set of challenging single loop benchmarks under Linear Integer Arithmetic.

Loops with multiple phases are challenging to verify because they require disjunctive invariants. Invariants could also have the form of implication between a precondition for the phase and a lemma that is valid throughout the phase. Such invariant structure is however not widely supported in state-of-the-art verification. We present a novel SMT-based approach to synthesize implication invariants for multi-phase loops. Our technique computes Model Based Projections to discover the program's phases and leverages data learning to get relationships among loop variables at an arbitrary place in the loop. It is effective in the challenging cases of mutually-dependent periodic phases, where many implication invariants need to be discovered simultaneously. Our approach has shown promising results in its ability to verify programs with complex phase structures. We have implemented and evaluated our algorithm against several state-of-the-art solvers.