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.

Conference Day
Tue 14 Apr

Displayed time zone: Azores change

14:00 - 16:00
Session 2ESOP at Skeel
Chair(s): Gavin BiermanOracle Labs
14:00
30m
Talk
Segment Abstraction for Worst-Case Execution Time Analysis
ESOP
Pavol CernyUniversity of Colorado Boulder, Thomas A. HenzingerIST Austria, Laura KovacsChalmers University of Technology, Arjun RadhakrishnaMicrosoft, Jakob ZwirchmayrIRIT Toulouse
14:30
30m
Talk
Automatic Static Cost Analysis for Parallel Programs
ESOP
Jan HoffmannYale University, Zhong ShaoYale University
15:00
30m
Talk
Sound, modular and compositional verification of the input/output behavior of programs
ESOP
Willem PenninckxKU Leuven, Bart JacobsiMinds - Distrinet, KU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven
15:30
30m
Talk
Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs
ESOP
Cristina DavidUniversity of Oxford, Daniel KroeningUniversity of Oxford, Matt LewisUniversity of Oxford