Algebra-based loop reasoning - invariant generation and synthesis for numeric loops

Abstract

Provably correct software is one of the key challenges in our software-driven society. Program verification – the task of proving correctness of a given program with respect to a given specification – and program synthesis – the task of constructing a program satisfying a given specification – are strategies for achieving this. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In both domains, handling loops is one of the main ingredients to a successful procedure. A so-called loop invariant is a property of a given loop describing its behavior, and is therefore the central notion for reasoning about program loops. In verification, the task is to compute invariants for a given loop, we call this task invariant generation. The reverse challenge, that is, synthesizing a loop which satisfies a given invariant, is called loop synthesis. We present algorithms for both scenarios based on techniques from the area of computer algebra. In particular, we develop techniques for generating invariants for numerical multi-path loops, and for the synthesis of numerical single-path loops. The central aspect in both settings is that we model loops as systems of recurrence equations. Every program variable of a loop induces a number sequence, and we reduce the invariant generation task to the task of computing the set of all algebraic relations among those sequences. In fact, we consider single-path loops whose variables induce number sequences which can be represented as a finite sum of hypergeometric sequences (so-called P-solvable sequences). We compute the invariants of multi-path loops by an iterative procedure employing Gröbner bases computations. Our approach computes the set of polynomial equality invariants of each program path and combines these ideals sequentially until a fixed point is reached. This fixed point represents the polynomial ideal of all polynomial invariants of the given P-solvable loop. We prove termination of our method and show that the maximal number of iterations for reaching the fixed point depends linearly on the number of program variables and the number of paths. The class of loops we are considering in loop synthesis can be modeled by a system of recurrence equations with constant coefficients (a subclass of P-solvable recurrences). We then turn the task of loop synthesis into a polynomial constraint problem by precisely characterizing the set of all loops satisfying a given set of polynomial equality invariants. Our approach is sound, and complete when the number of auxiliary variables is bounded. Furthermore, we show that it can be automated by leveraging SMT solvers for solving our polynomial constraint problems. The combination of the two techniques provides a strong foundation for a successful procedure in the context of loop optimizations such as strength reduction.