Synthesizing Ranking Functions from Bits and Pieces.

In this work, we present a novel approach based on recent advances in software model checking to synthesize ranking functions and prove termination and non-termination of imperative programs. Our approach incrementally refines a termination argument from an under-approximation of the terminating program state. Specifically, we learn bits of information from terminating executions, and from these we extrapolate ranking functions over-approximating the number of loop iterations needed for termination. We combine these pieces into piecewise-defined, lexicographic, or multiphase ranking functions. The proposed technique has been implemented in SeaHorn --- an LLVM based verification framework --- targeting C code. Preliminary experimental evaluation demonstrated its effectiveness in synthesizing ranking functions and proving termination of C programs.