Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs

Caterina Urban 1
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
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.
Document type :
Theses
Complete list of metadatas

Cited literature [99 references]  Display  Hide  Download

https://tel.archives-ouvertes.fr/tel-01176641
Contributor : Urban Caterina <>
Submitted on : Wednesday, July 15, 2015 - 4:21:53 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Wednesday, April 26, 2017 - 5:43:22 AM

File

Identifiers

  • HAL Id : tel-01176641, version 1

Citation

Caterina Urban. Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs. Computer Science [cs]. École Normale Supérieure, 2015. English. ⟨tel-01176641v1⟩

Share

Metrics

Record views

692

Files downloads

388