ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Tue 14 Apr 2015 14:30 - 15:00 at Skeel - Session 2 Chair(s): Gavin Bierman

This article introduces the first automatic analysis for deriving bounds on the worst-case evaluation cost of parallel first-order functional programs. The analysis is performed by a novel type system for amortized resource analysis. The main innovation is a technique that separates the reasoning about sizes of data structures and evaluation cost within the same framework. The cost semantics of parallel programs is based on call-by-value evaluation and the standard cost measures work and depth. A soundness proof of the type system establishes the correctness of the derived cost bounds with respect to the cost semantics. The derived bounds are multivariate resource polynomials which depend on the sizes of the arguments of a function.

Tue 14 Apr

Displayed time zone: Azores change

14:00 - 16:00
Session 2ESOP at Skeel
Chair(s): Gavin Bierman Oracle Labs
14:00
30m
Talk
Segment Abstraction for Worst-Case Execution Time Analysis
ESOP
Pavol Cerny University of Colorado Boulder, Thomas A. Henzinger IST Austria, Laura Kovacs Chalmers University of Technology, Arjun Radhakrishna Microsoft, Jakob Zwirchmayr IRIT Toulouse
14:30
30m
Talk
Automatic Static Cost Analysis for Parallel Programs
ESOP
Jan Hoffmann Yale University, Zhong Shao Yale University
15:00
30m
Talk
Sound, modular and compositional verification of the input/output behavior of programs
ESOP
Willem Penninckx KU Leuven, Bart Jacobs iMinds - Distrinet, KU Leuven, Frank Piessens iMinds - Distrinet, KU Leuven
15:30
30m
Talk
Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
ESOP
Cristina David University of Oxford, Daniel Kroening University of Oxford, Matt Lewis University of Oxford