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

In the standard framework for worst-case execution time analysis of programs, the main data structure is a single instance integer linear programming that represents the whole program. The instance of this NP-hard problem must be solved to find an estimate for WCET, and it must be refined if the estimate is not tight. We propose a new framework for WCET analysis, based on abstract segment trees (ASTs) as the main data structure. The ASTs have two advantages. First, they allow computing WCET by solving a number of independent small ILP instances. Second, ASTs store more expressive constraints, thus enabling a more efficient and precise refinement procedure. In order to realize our framework algorithmically, we develop an algorithm for WCET estimation on ASTs, and we develop an interpolation-based counterexample-guided refinement scheme for ASTs.

Tue 14 Apr
Times are displayed in time zone: Azores change

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