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.
Wed 17 JunDisplayed time zone: Tijuana, Baja California change
14:00 - 15:40 | |||
14:00 25mTalk | Automatic Induction Proofs of Data-Structures in Imperative Programs Research Papers Duc-Hiep Chu National University of Singapore, Joxan Jaffar National University of Singapore, Minh-Thai Trinh National University of Singapore Media Attached | ||
14:25 25mTalk | Compositional Certified Resource Bounds Research Papers Link to publication Media Attached | ||
14:50 25mTalk | Peer-to-peer Affine Commitment using Bitcoin Research Papers Media Attached | ||
15:15 25mTalk | Termination and Non-Termination Specification Inference Research Papers Ton Chanh Le National University of Singapore, Shengchao Qin Teesside University, Wei-Ngan Chin National University of Singapore Media Attached |