Non-linear reasoning for invariant synthesis
Abstract
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).
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 27, 2017
- Source ID
- 10.1145/3158142
Entities
People
- Jason Breck
- John Cyphert
- Thomas Reps
- Zachary Kincaid
Organizations
- Defense Advanced Research Projects Agency
- Princeton University
- University of Wisconsin–Madison
- Wisconsin Alumni Research Foundation