Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs

TL;DR

This paper introduces a novel termination analysis method that generates nonlinear ranking functions and recurrence sets, applicable to fixed-width machine and floating-point arithmetic, overcoming limitations of linear approaches.

Contribution

It presents a new approach using second-order logic reduction to handle nonlinear termination arguments for finite-state programs.

Findings

Sound and complete for fixed-width integers

Applicable to IEEE floating-point arithmetic

Handles nonlinear and lexicographic ranking functions

Abstract

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 \emph{termination} to second-order \emph{satisfaction}. We provide formulations for termination and non-termination in a fragment of second-order logic with restricted quantification which is decidable over finite domains. 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.