Termination analysis without the tears

Shaowei Zhu, Zachary Kincaid

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

Abstract

Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis may be classified into two groups: (1) algorithms with strong behavioral guarantees that work in limited circumstances (e.g., complete synthesis of linear ranking functions for polyhedral loops), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (e.g., Terminator). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees? This paper presents a termination analysis that is both compositional (the result of analyzing a composite program is a function of the analysis results of its components) and monotone ("more information into the analysis yields more information out"). The paper has two key contributions. The first is an extension of Tarjan's method for solving path problems in graphs to solve infinite path problems. This provides a foundation upon which to build compositional termination analyses. The second is a collection of monotone conditional termination analyses based on this framework. We demonstrate that our tool ComPACT (Compositional and Predictable Analysis for Conditional Termination) is competitive with state-of-the-art termination tools while providing stronger behavioral guarantees.

Original languageEnglish (US)
Title of host publicationPLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
EditorsStephen N. Freund, Eran Yahav
PublisherAssociation for Computing Machinery
Pages1296-1311
Number of pages16
ISBN (Electronic)9781450383912
DOIs
StatePublished - Jun 18 2021
Event42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021 - Virtual, Online, Canada
Duration: Jun 20 2021Jun 25 2021

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
Country/TerritoryCanada
CityVirtual, Online
Period6/20/216/25/21

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • algebraic path problems
  • Algebraic program analysis
  • loop summarization
  • termination analysis

Fingerprint

Dive into the research topics of 'Termination analysis without the tears'. Together they form a unique fingerprint.

Cite this