POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 10:55 - 11:20 at Amphitheater 44 - Program Analysis Chair(s): Francesco Logozzo

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. as steps ≤ ? ∗ size(l) + ? in the contracts of functions, as well as express invariants necessary for establishing the bounds that may possibly depend on the state of memoization. Our approach operates in two phases: first generating an instrumented first-order program that accurately models the higher-order control flow, and the effects of memoization on resources, using sets, algebraic datatypes, and mutual recursion, and then verifying the contracts of the first-order program by producing verification conditions (VCs) of the form exists-forall using an extended assume/guarantee reasoning. We use our approach to verify precise bounds on resources such as evaluation steps, and number of heap-allocated objects, on 17 challenging data structures and algorithms. Our benchmarks, comprising of 5K lines of functional Scala code, include lazy mergesort, Okasaki’s real- time queue and deque data structures that rely on aliasing of references to first-class functions; lazy data structures based on numerical representations such as the conqueue data structure of Scala’s data-parallel library, cyclic streams such as hamming number sequence, as well as dynamic programming algorithms like Levenstein distance, Viterbi algorithm, and packrat parsing. Our evaluations show that, when averaged over all benchmarks, the actual runtime resource consumption is at least 80% of the value inferred by our tool when estimating the number of evaluation steps, and is at least 88% for the number of heap-allocated objects.

Thu 19 Jan

POPL-2017-papers
10:30 - 12:10: POPL - Program Analysis at Amphitheater 44
Chair(s): Francesco LogozzoFacebook
POPL-2017-papers10:30 - 10:55
Talk
Ezgi ÇiçekMPI-SWS, Germany, Gilles BartheIMDEA, Marco GaboardiSUNY Buffalo, USA, Deepak GargMPI-SWS, Germany, Jan HoffmannCarnegie Mellon University
POPL-2017-papers10:55 - 11:20
Talk
Ravichandhran MadhavanEPFL, Sumith KulalIIT Bombay, Viktor KunčakEPFL, Switzerland
POPL-2017-papers11:20 - 11:45
Talk
Qirun ZhangUniversity of California, Davis, Zhendong SuUniversity of California, Davis
POPL-2017-papers11:45 - 12:10
Talk
Jan HoffmannCarnegie Mellon University, Ankush DasCarnegie Mellon University, Shu-chun WengYale University