Termination and non-termination specification inference

Ton Chanh Le, Shengchao Qin, Wei-Ngan Chin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

138 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationPLDI '15 Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
Place of PublicationNew York, USA
PublisherACM
Pages489-498
Volume50
Edition6
ISBN (Electronic)978-1-4503-3468-6
DOIs
Publication statusPublished - Jun 2015
Event36th ACM SIGPLAN Conference on Programming Language Design and Implementation - Portland, United States
Duration: 13 Jun 201517 Jun 2015

Conference

Conference36th ACM SIGPLAN Conference on Programming Language Design and Implementation
Abbreviated titlePLDI '15
CountryUnited States
CityPortland
Period13/06/1517/06/15

Fingerprint Dive into the research topics of 'Termination and non-termination specification inference'. Together they form a unique fingerprint.

  • Cite this

    Le, T. C., Qin, S., & Chin, W-N. (2015). Termination and non-termination specification inference. In PLDI '15 Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (6 ed., Vol. 50, pp. 489-498). ACM. https://doi.org/10.1145/2737924.2737993