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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Program AnalysisPOPL at Amphitheater 44
Chair(s): Francesco Logozzo Facebook
10:30
25m
Talk
Relational Cost Analysis
POPL
Ezgi Çiçek MPI-SWS, Germany, Gilles Barthe IMDEA, Marco Gaboardi SUNY Buffalo, USA, Deepak Garg MPI-SWS, Germany, Jan Hoffmann Carnegie Mellon University
10:55
25m
Talk
Contract-based Resource Verification for Higher-order Functions with Memoization
POPL
Ravichandhran Madhavan EPFL, Sumith Kulal IIT Bombay, Viktor Kunčak EPFL, Switzerland
11:20
25m
Talk
Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
POPL
Qirun Zhang University of California, Davis, Zhendong Su University of California, Davis
11:45
25m
Talk
Towards Automatic Resource Bound Analysis for OCaml
POPL
Jan Hoffmann Carnegie Mellon University, Ankush Das Carnegie Mellon University, Shu-chun Weng Yale University