Wed 17 Jun 2015 15:15 - 15:40 at PLDI Main RED (Portland 256) - Logic Chair(s): Nate Foster

Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non-termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method. This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against state-of-the-art termination analyzers.

PLDI 2015 Artifact Evaluated Badge

Wed 17 Jun
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

14:00 - 15:40: Research Papers - Logic at PLDI Main RED (Portland 256)
Chair(s): Nate FosterCornell University
pldi2015-papers14:00 - 14:25
Duc-Hiep ChuNational University of Singapore, Joxan JaffarNational University of Singapore, Minh-Thai TrinhNational University of Singapore
Media Attached
pldi2015-papers14:25 - 14:50
Quentin CarbonneauxYale University, Jan HoffmannYale University, Zhong ShaoYale University
Link to publication Media Attached
pldi2015-papers14:50 - 15:15
Karl CraryCarnegie Mellon University, Michael J. Sullivan
Media Attached
pldi2015-papers15:15 - 15:40
Ton Chanh LeNational University of Singapore, Shengchao QinTeesside University, Wei-Ngan ChinNational University of Singapore
Media Attached