Abstract

Program termination is the most prominent liveness property. We design new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize piecewise-defined ranking functions, which provide upper bounds on the waiting time before termination. We also contributes an abstract interpretation framework for proving liveness properties, which comes as a generalization of the framework proposed for termination. In particular, the framework is dedicated to liveness properties expressed in temporal logic, which are used to ensure that some desirable event happens once or infinitely many times during program execution. The results presented in this talk have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks and it is competitive with the state of the art.