The ability of program-analysis tools to identify program invariants is hampered by the capabilities of present-day solvers for handling non-linear arithmetic—including polynomials, exponentials, and logarithms. Improved capabilities for reasoning about non-linear functions would help program analyzers establish important program invariants. For instance, reasoning about exponentials provides a way to find invariants of digital-filter programs; reasoning about polynomials and/or logarithms is needed for establishing invariants that describe the time or memory usage of many well-known algorithms. This paper describes the techniques used in an arithmetic-reasoning kit to represent logarithmic and exponential relationships indirectly, using uninterpreted-function symbols and integrity constraints. It also describes a recurrence-relation solver—used to find invariants of loops—that handles two classes of recurrences: * Ones of the form $x_{n+1} = b*x_n + f(n)$, where $b$ is a constant, and $f(n)$ is a sum of polynomials, exponentials, or products of a polynomial and an exponential. * Ones of the form $\mathbf{y_{n+1}} = \mathbf{A}\mathbf{y_n} + \mathbf{f(n)}$, where $\mathbf{y_n}$ is a vector of variables, $\mathbf{A}$ is a rational matrix, and $\mathbf{f(n)}$ is a vector of functions, where each entry is a sum of polynomials, exponentials, or products of a polynomial and an exponential.

Our technique has been implemented in a program analyzer that can analyze general loops—including loops that contain branches and nested loops—and mutually recursive functions. Our experiments show that our technique shows promise for non-linear assertion-checking and resource-bound generation.

#### Fri 12 Jan

13:30 - 13:40Awards | Benjamin DelawarePurdue University | |||||||||||||||||||||||||||||||||||||||||

13:30 - 13:52Talk | Niki VazouUniversity of Maryland, Anish TondwalkarUCSD, Vikraman Choudhury, Ryan ScottIndiana University, Ryan R. NewtonIndiana University, Philip WadlerUniversity of Edinburgh, UK, Ranjit JhalaUniversity of California, San Diego | |||||||||||||||||||||||||||||||||||||||||

14:05 - 14:30Talk | Zachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc. | |||||||||||||||||||||||||||||||||||||||||

14:30 - 14:55Talk | ||||||||||||||||||||||||||||||||||||||||||

14:55 - 15:20Talk | Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu K. LahiriMicrosoft Research, William CookUniversity of Texas at Austin |