Unrestricted termination and non-termination arguments for bit-vector programs

DOI10.1007/978-3-662-46669-8_8zbMATH Open1335.68050arXiv1410.5089OpenAlexW2161089445MaRDI QIDQ2802436FDOQ2802436

Authors: Cristina David, Daniel Kroening, Matthew A. Lewis 

Publication date: 26 April 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1410.5089

Recommendations

• Proving termination of programs with bitvector arithmetic by symbolic execution
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• scientific article; zbMATH DE number 1903370
• On the linear ranking problem for simple floating-point loops
• Ranking function synthesis for bit-vector relations

zbMATH Keywords

terminationnon-terminationbit-vector ranking functionsfloating-point ranking functionslexicographic ranking functions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (5)

• \textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches
• Termination of floating-point computations
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Automatically proving termination and memory safety for programs with pointer arithmetic

This page was built for publication: Unrestricted termination and non-termination arguments for bit-vector programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802436)