Séminaire APRRSS

Séminaire APR: Synthesizing Ranking Functions From Bits and Pieces

https://people.inf.ethz.ch/caurban/Home.html
26/01/2017
Intervenant(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.

Plus d'informations ici …
Mentions légales
Carte du site