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

Abstract. Proving program termination is typically done by finding a well-founded ranking function for the program states. Existing termina-tion provers typically find ranking functions using either linear algebra or templates. As such they are often restricted to finding linear rank-ing functions over mathematical integers. This class of functions is in-sufficient for proving termination of many terminating programs, and furthermore a termination argument for a program operating on mathe-matical 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 rank-ing 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 termination to second-order sat-isfaction. We provide formulations for termination and non-termination in a fragment of second-order logic with restricted quantification which is decidable over finite domains [1]. The resulting technique is a sound and complete analysis for the termination of finite-state programs with fixed-width integers and IEEE floating-point arithmetic