Non-linear Reasoning for Invariant Synthesis
Z. Kincaid, J. Cyphert, J. Breck, and T. Reps
Automatic generation of non-linear loop invariants is a long-standing
challenge in program analysis, with many applications. For instance, reasoning
about exponentials provides a way to find invariants of digital-filter
programs, and reasoning about polynomials and/or logarithms is needed for
establishing invariants that describe the time or memory usage of many
well-known algorithms. An appealing approach to this challenge is to exploit
the powerful recurrence-solving techniques that have been developed in the
field of computer algebra, which can compute exact characterizations of
non-linear repetitive behavior. However, there is a gap between the
capabilities of recurrence solvers and the needs of program analysis: (1) loop
bodies are not merely systems of recurrence relations---they may contain
conditional branches, nested loops, non-deterministic assignments, etc., and
(2) a client program analyzer must be able to reason about the closed-form
solutions produced by a recurrence solver (e.g., to prove assertions).
This paper presents a method for generating non-linear invariants of general
loops based on analyzing recurrence relations. The key components are an
abstract domain for reasoning about non-linear arithmetic, a semantics-based
method for extracting recurrence relations from loop bodies, and a recurrence
solver that avoids closed forms that involve complex or irrational numbers.
Our technique has been implemented in a program analyzer that can analyze
general loops and mutually recursive procedures. Our experiments show that
our technique shows promise for non-linear assertion-checking and
resource-bound generation.
(Click here to access the paper:
PDF.)