Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Fri 19 Jun 2020 11:20 - 11:40 at PLDI Research Papers live stream - Verification II Chair(s): Manu Sridharan

This paper is the confluence of two streams of ideas in the literature on generating numerical invariants, namely: (1) template-based methods, and (2) recurrence-based methods.

A \emph{template-based method} begins with a template that contains unknown quantities, and finds invariants that match the template by extracting and solving constraints on the unknowns. A disadvantage of template-based methods is that they require fixing the set of terms that may appear in an invariant in advance. This disadvantage is particularly prominent for non-linear invariant generation, because the user must supply maximum degrees on polynomials, bases for exponents, etc.

On the other hand, \emph{recurrence-based methods} are able to find sophisticated non-linear mathematical relations, including polynomials, exponentials, and logarithms, because such relations arise as the solutions to recurrences. However, a disadvantage of past recurrence-based invariant-generation methods is that they are primarily loop-based analyses: they use recurrences to relate the pre-state and post-state of a loop, so it is not obvious how to apply them to a recursive procedure, especially if the procedure is \emph{non-linearly recursive} (e.g., a tree-traversal algorithm).

In this paper, we combine these two approaches and obtain a technique that uses templates in which the unknowns are \textit{functions} rather than numbers, and the constraints on the unknowns are \textit{recurrences}. The technique synthesizes invariants involving polynomials, exponentials, and logarithms, even in the presence of arbitrary control-flow, including any combination of loops, branches, and (possibly non-linear) recursion. For instance, it is able to show that (i) the time taken by merge-sort is $O(n \log(n))$, and (ii) the time taken by Strassen's algorithm is $O(n^{\log_2(7)})$.

Fri 19 Jun

Displayed time zone: Pacific Time (US & Canada) change

10:40 - 12:00
Verification IIPLDI Research Papers at PLDI Research Papers live stream
Chair(s): Manu Sridharan University of California Riverside

YouTube lightning session video

10:40
20m
Talk
Scalable Validation of Binary Lifters
PLDI Research Papers
Sandeep Dasgupta University of Illinois at Urbana-Champaign, USA, Sushant Dinesh University of Illinois at Urbana-Champaign, USA, Deepan Venkatesh University of Illinois at Urbana-Champaign, USA, Vikram S. Adve University of Illinois at Urbana-Champaign, USA, Christopher W. Fletcher University of Illinois at Urbana-Champaign, USA
11:00
20m
Talk
Polynomial Invariant Generation for Non-deterministic Recursive Programs
PLDI Research Papers
Krishnendu Chatterjee IST Austria, Austria, Hongfei Fu Shanghai Jiao Tong University, China, Amir Kafshdar Goharshady IST Austria, Austria, Ehsan Kafshdar Goharshady Ferdowsi University of Mashhad, Iran
11:20
20m
Talk
Templates and Recurrences: Better Together
PLDI Research Papers
Jason Breck University of Wisconsin-Madison, USA, John Cyphert University of Wisconsin-Madison, USA, Zachary Kincaid Princeton University, USA, Thomas Reps University of Wisconsin-Madison, USA
11:40
20m
Talk
First-Order Quantified Separators
PLDI Research Papers
Jason R. Koenig Stanford University, USA, Oded Padon Stanford University, USA, Neil Immerman University of Massachusetts at Amherst, USA, Alex Aiken Stanford University, USA