This report presents the bulk of my research work from the completion of my PhD, in late 2004, until the present day. The overall aim of my research is the development of mathematically sound and practically efficient methods to check the correctness of computer software. Efficiency is achieved using approximations, while soundness is guaranteed by employing over-approximations of program behaviors. My research is grounded in the theory of abstract interpretation, a powerful mathematical framework facilitating the development, use, comparison, and composition of approximations in a sound way. I am mainly interested in developing new reusable abstraction components (so called abstract domains) that can be readily implemented, and in using them to develop static analyzers, which are computer programs able to check automatically the safety of software. While my early research was focused on inferring the values of variables in sequential programs, my current interest and latest results concern the analysis of concurrent programs, hence the title of this report. The first two chapters of this report constitute an introduction. The first chapter is an informal introduction to the problem at hand, existing solutions, their strengths and their shortcomings. The second chapter presents prior mathematical and formal tools on which our work is based, including some notions of abstract interpretation, a description of existing abstract domains and their application to the static analysis of sequential programs. It also recalls some results I obtained during my PhD and that will be useful in the rest of the report. The subsequent chapters describe the work I performed after completing my PhD. The third chapter is devoted to aspects of static analyzers that are specific to concurrent programs. This topic of personal research has led to the construction of a generic analysis method for concurrent programs, parametrized by the choice of abstract domains. The method is based on a notion of ''interference'' that abstracts thread interleavings in a sound way in order to achieve a thread-modular analysis. It is related to Jones' rely-guarantee proof method, and we make this connection formal in a first part. Then, we present an interference-based analysis in big-step form that is efficient and easy to implement. In a third part, we study the interaction of the analysis with weakly consistent memory models, found in modern processors and language specifications. The last part discusses how to adapt the analysis to exploit some properties of the scheduling (such as the use of real-time thread priorities and synchronization primitives). The fourth and fifth chapters are devoted to the design of abstract domains. Although some of them found their application in the analysis of concurrent programs, they are actually generic and could be exploited in any kind of static analysis, for concurrent or sequential programs. The fourth chapter concerns numeric domains to infer linear equality and inequality relations, developed in collaboration with Liqian Chen while he visited ENS during his PhD. The initial motivation was to revise the classic polyhedra domain using sound floating-point arithmetic to improve its efficiency, but it unexpectedly yielded the construction of new, more expressive domains based on interval affine relations, which we also present. The fifth chapter concerns the abstraction of realistic data-types as found in the C programming language, including machine integers, floating-point numbers, and structured blocks of memory (structs, unions, and arrays). We design abstractions that are aware of the low-level memory representation of data-types, to support the analysis of programs that rely on assumptions about this representation (such as ''type punning'' constructions in C). The need for such abstractions was motivated by the analysis, in the scope of the Astrée and AstréeA static analyzers, of industrial C programs, where such low-level constructions are widespread. The sixth chapter is devoted to the application of these methods to the design of static analyzer tools. It mainly reports on my experience with the Astrée analyzer, a team effort initiated during my PhD in 2001 that extended well beyond it and culminated in its industrialization in 2009. Much of my theoretical work could find some application in Astrée, as Astrée fuelled my research with not only practical problems to solve, but also concrete problems that could only be overcome by theoretical developments. This part also reports my own ongoing effort on AstréeA, an extension of Astrée that incorporates the interference abstraction presented above and aims at proving the absence of run-time error in concurrent embedded programs (while Astrée only considers synchronous programs). Additionally, this chapter presents the Apron abstract domain library, another, more academic, team effort, which aims at encouraging the research on numeric abstract domains. The report concludes with some perspectives for future researches.
Static analysis by abstract interpretation of concurrent programs