Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs

Caterina Urban

Abstract

The overall aim of this thesis is the development of mathematically sound and practically ecient methods for automatically proving the correctness of computer software. More specifically, this thesis is grounded in the theory of Abstract Interpretation, a powerful mathematical framework for approximating the behavior of programs. In particular, this thesis focuses on proving program liveness properties, which represent requirements that must be eventually or repeatedly realized during program execution.

Program termination is the most prominent liveness property. This thesis designs new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize so called piecewise- defined ranking functions, which provide upper bounds on the waiting time before termination. The approximations are parametric in the choice between the expressivity and the cost of the underlying approximations, which maintain information about the set of possible values of the program variables along with the possible numerical relationships between them.

This thesis 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. As for program termination, piecewise-defined ranking functions are used to infer sufficient preconditions for these properties, and to provide upper bounds on the waiting time before a desirable event.

The results presented in this thesis have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art, and is able to analyze programs that are out of the reach of existing methods.