2014/10/19 by Cristina David, David, Cristina, Daniel Kroening +5
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1410.5089
openalex publication_date 2014/10/19 · openalex created_date 2022/10/03 · openalex updated_date 2026/07/28
Proving program termination is typically done by finding a well-founded\nranking function for the program states. Existing termination provers typically\nfind ranking functions using either linear algebra or templates. As such they\nare often restricted to finding linear ranking functions over mathematical\nintegers. This class of functions is insufficient for proving termination of\nmany terminating programs, and furthermore a termination argument for a program\noperating on mathematical integers does not always lead to a termination\nargument for the same program operating on fixed-width machine integers. We\npropose a termination analysis able to generate nonlinear, lexicographic\nranking functions and nonlinear recurrence sets that are correct for\nfixed-width machine arithmetic and floating-point arithmetic Our technique is\nbased on a reduction from program \termination to second-order\n\satisfaction. We provide formulations for termination and\nnon-termination in a fragment of second-order logic with restricted\nquantification which is decidable over finite domains. The resulted technique\nis a sound and complete analysis for the termination of finite-state programs\nwith fixed-width integers and IEEE floating-point arithmetic.\n