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 13:30 - 13:40Awards SRC AwardsBenjamin DelawarePurdue University 13:30 - 13:52Talk Refinement Reflection: Complete Verification with SMTNiki 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 Non-Linear Reasoning For Invariant SynthesisZachary KincaidPrinceton University, John CyphertUniversity of Wisconsin - Madison, Jason BreckUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc. 14:30 - 14:55Talk A Practical Construction for Decomposing Numerical Abstract DomainsGagandeep Singh, Markus PüschelETH Zürich, Martin VechevETH Zürich 14:55 - 15:20Talk Verifying Equivalence of Database-Driven ApplicationsYuepeng WangUniversity of Texas at Austin, Isil DilligUT Austin, Shuvendu K. LahiriMicrosoft Research, William CookUniversity of Texas at Austin