Séminaire APR: Synthesizing Ranking Functions From Bits and Pieces
Speaker(s) : Caterina Urban (ETH Zurich, Switzerland)
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.