This paper presents a new method for automatically generating numerical invariants for imperative programs. Given a program, our procedure computes a binary input output relation on program states which over-approximates the behaviour of the program. It is compositional in the sense that it operates by decomposing the program into parts, computing an abstract meaning of each part, and then composing the meanings. Our method for approximating loop behaviour is based on first approximating the meaning of the loop body, extracting recurrence relations from that approximation, and then using the closed forms to approximate the loop. Our experiments demonstrate that on verification tasks, our method is competitive with leading invariant generation and verification tools.
Ammarguellat and Harrison present a method for detecting induction variables which is compositional in the sense that it uses closed forms for inner loops in order to recognize nested recurrences @cite_29 . Maps from variables to symbolic terms (effectively a symbolic constant propagation domain) is used as the abstract domain. Kov ' a cs presents a technique for discovering invariant polynomial equations based on solving recurrence relations @cite_11 . The simple and stratified recurrence equations considered in this paper are a strict subset of the recurrences considered in @cite_11 , but our algorithm for solving recurrences is simpler. @cite_19 presents a technique for computing -approximations of loops which uses polynomial curve-fitting to directly compute closed forms for recurrences rather than extracting recurrences and then solving them in a separate step.
@cite_19 @cite_29 @cite_11
2218365969 2044738061 1585981132
Many software model checkers only detect counterexamples with deep loops after exploring numerous spurious and increasingly longer counterexamples. We propose a technique that aims at eliminating this weakness by constructing auxiliary paths that represent the effect of a range of loop iterations. Unlike acceleration, which captures the exact effect of arbitrarily many loop iterations, these auxiliary paths may under-approximate the behaviour of the loops. In return, the approximation is sound with respect to the bit-vector semantics of programs. Our approach supports arbitrary conditions and assignments to arrays in the loop body, but may as a result introduce quantified conditionals. To reduce the resulting performance penalty, we present two quantifier elimination techniques specially geared towards our application. Loop under-approximation can be combined with a broad range of verification techniques. We paired our techniques with lazy abstraction and bounded model checking, and evaluated the resulting tool on a number of buffer overflow benchmarks, demonstrating its ability to efficiently detect deep counterexamples in C programs that manipulate arrays. The recognition of recurrence relations is important in several ways to the compilation of programs. Induction variables, the simplest form of recurrence, are pivotal in loop optimizations and dependence testing. Many recurrence relations, although expressed sequentially by the programmer, lend themselves to efficient vector or parallel computation. Despite the importance of recurrences, vectorizing and parallelizing compilers to date have recognized them only in an ad-hoc fashion. In this paper we put forth a systematic method for recognizing recurrence relations automatically. Our method has two parts. First, abstract interpretation [CC77, CC79] is used to construct a map that associates each variable assigned in a loop with a symbolic form (expression) of its value. Second, the elements of this map are matched with patterns that describe recurrence relations. The scheme is easily extensible by the addition of templates, and is able to recognize nested recurrences by the propagation of the closed forms of recurrences from inner loops. We present some applications of this method and a proof of its correctness. We present a method for generating polynomial invariants for a subfamily of imperative loops operating on numbers, called the P-solvable loops. The method uses algorithmic combinatorics and algebraic techniques. The approach is shown to be complete for some special cases. By completeness we mean that it generates a set of polynomial invariants from which, under additional assumptions, any polynomial invariant can be derived. These techniques are implemented in a new software package Aligator written in Mathematica and successfully tried on many programs implementing interesting algorithms working on numbers.