Fri 12 Jan 2018 14:05 - 14:30 at Bunker Hill - Program Analysis II Chair(s): Işıl 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 JanDisplayed time zone: Tijuana, Baja California change

 13:30 - 15:20 Program Analysis IIResearch Papers at Bunker Hill Chair(s): Işıl Dillig UT Austin 13:3010mAwards SRC AwardsResearch PapersBenjamin Delaware Purdue University 13:3022mTalk Refinement Reflection: Complete Verification with SMTResearch PapersNiki Vazou University of Maryland, Anish Tondwalkar UCSD, Vikraman Choudhury , Ryan Scott Indiana University, Ryan R. Newton Indiana University, Philip Wadler University of Edinburgh, UK, Ranjit Jhala University of California, San Diego 14:0525mTalk Non-Linear Reasoning For Invariant SynthesisResearch PapersZachary Kincaid Princeton University, John Cyphert University of Wisconsin - Madison, Jason Breck University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. 14:3025mTalk A Practical Construction for Decomposing Numerical Abstract DomainsResearch PapersGagandeep Singh , Markus Püschel ETH Zürich, Martin Vechev ETH Zürich 14:5525mTalk Verifying Equivalence of Database-Driven ApplicationsResearch PapersYuepeng Wang University of Texas at Austin, Işıl Dillig UT Austin, Shuvendu K. Lahiri Microsoft Research, William Cook University of Texas at Austin