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 AprDisplayed time zone: Azores change
Tue 14 Apr
Displayed time zone: Azores change
14:00 - 16:00 | |||
14:00 30mTalk | 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 30mTalk | Automatic Static Cost Analysis for Parallel Programs ESOP | ||
15:00 30mTalk | 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 30mTalk | 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 |