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
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

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

YouTube lightning session video

pldi-2020-papers10:40 - 11:00
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Sushant DineshUniversity of Illinois at Urbana-Champaign, USA, Deepan VenkateshUniversity of Illinois at Urbana-Champaign, USA, Vikram S. AdveUniversity of Illinois at Urbana-Champaign, USA, Christopher W. FletcherUniversity of Illinois at Urbana-Champaign, USA
pldi-2020-papers11:00 - 11:20
Krishnendu ChatterjeeIST Austria, Austria, Hongfei FuShanghai Jiao Tong University, China, Amir Kafshdar GoharshadyIST Austria, Austria, Ehsan Kafshdar GoharshadyFerdowsi University of Mashhad, Iran
pldi-2020-papers11:20 - 11:40
Jason BreckUniversity of Wisconsin-Madison, USA, John CyphertUniversity of Wisconsin-Madison, USA, Zachary KincaidPrinceton University, USA, Thomas RepsUniversity of Wisconsin-Madison, USA
pldi-2020-papers11:40 - 12:00
Jason R. KoenigStanford University, USA, Oded PadonStanford University, USA, Neil ImmermanUniversity of Massachusetts at Amherst, USA, Alex AikenStanford University, USA