Fri 12 Jan 2018 14:05 - 14:30 at Bunker Hill - Program Analysis II Chair(s): Isil Dillig

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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:30 - 15:20: Research Papers - Program Analysis II at Bunker Hill
Chair(s): Isil DilligUT Austin
POPL-2018-papers13:30 - 13:40
Benjamin DelawarePurdue University
POPL-2018-papers13:30 - 13:52
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
POPL-2018-papers14:05 - 14:30
Zachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
POPL-2018-papers14:30 - 14:55
POPL-2018-papers14:55 - 15:20
Yuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu K. LahiriMicrosoft Research, William CookUniversity of Texas at Austin