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

Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termination provers typically find ranking functions using either linear algebra or templates. As such they are often restricted to finding linear ranking functions over mathematical integers. This class of functions is insufficient for proving termination of many terminating programs, and furthermore a termination argument for a program operating on mathematical integers does not always lead to a termination argument for the same program operating on fixed-width machine integers. We propose a termination analysis able to generate nonlinear, lexicographic ranking functions and nonlinear recurrence sets that are correct for fixed-width machine arithmetic and floating-point arithmetic Our technique is based on a reduction from program termination to second-order satisfaction. The resulted technique is a sound and complete analysis for the termination of finite-state programs with fixed-width integers and IEEE floating-point arithmetic.

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

14:00 - 16:00: ESOP - Session 2 at Skeel
Chair(s): Gavin BiermanOracle Labs
esop-2015-papers14:00 - 14:30
Pavol CernyUniversity of Colorado Boulder, Thomas A. HenzingerIST Austria, Laura KovacsChalmers University of Technology, Arjun RadhakrishnaMicrosoft, Jakob ZwirchmayrIRIT Toulouse
esop-2015-papers14:30 - 15:00
Jan HoffmannYale University, Zhong ShaoYale University
esop-2015-papers15:00 - 15:30
Willem PenninckxKU Leuven, Bart JacobsiMinds - Distrinet, KU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven
esop-2015-papers15:30 - 16:00
Cristina DavidUniversity of Oxford, Daniel KroeningUniversity of Oxford, Matt LewisUniversity of Oxford