Search

International audience; In this document, we use the Abstract Interpretation framework to analyze concurrent programs using Thread-Modular Analysis. We designed a relational abstraction of interferences in order to infer more properties and go beyond the state of the art. We implemented a basic analyzer, studying the numerical properties of a simple language. We present the results obtained, as well as a study of the scalability of this approach.

International audience; We study thread-modular static analysis by abstract interpretation to infer the values of variables in concurrent programs. We show how to go beyond the state of the art and increase an analysis precision by adding the ability to infer some relational and history-sensitive properties of thread interferences. The fundamental basis of this work is the formalization by abstract interpretation of a rely-guarantee concrete semantics which is thread-modular, constructive, and complete for safety properties. We then show that previous analyses based on non-relational interferences can be retrieved as coarse computable abstractions of this semantics; additionally, we present novel abstraction examples exploiting our ability to reason more precisely about interferences, including domains to infer relational lock invariants and the monotonicity of counters. Our method and domains have been implemented in the AstréeA static analyzer that checks for run-time errors in embedded concurrent C programs, where they enabled a significant reduction of the number of false alarms.

International audience; This book constitutes the refereed proceedings of the 15th International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI 2014, held in San Diego, CA, USA, in January 2013. The 25 revised full papers presented were carefully reviewed and selected from 64 submissions. The papers cover a wide range of topics including program verification, model checking, abstract interpretation and abstract domains, program synthesis, static analysis, type systems, deductive methods, program certification, debugging techniques, program transformation, optimization, hybrid and cyber-physical systems.

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., Ce mémoire d'habilitation résume la majeure partie de mes recherches, depuis la fin de mon doctorat, fin 2004, jusqu'à aujourd'hui. Le but essentiel de mes recherches est le développement de méthodes fondées sur des bases mathématiques et performantes en pratique pour s'assurer de la correction des logiciels. J'utilise des approximations pour permettre une bonne performance, tandis que la validité des résultats est garantie par l'emploi exclusif de sur-approximations des ensembles des comportements des programmes. Ma recherche est basée sur l'interprétation abstraite, une théorie très puissante des approximations de sémantiques permettant aisément de les développer, les comparer, les combiner. Je m'emploie en particulier au développement de nouveaux composants réutilisables d'abstraction, les domaines abstraits, qui sont directement implantables en machine, ainsi qu'à leur utilisation au sein d'analyseurs statiques, qui sont des outils de vérification automatique de programmes. Mes premières recherches concernaient l'inférence de propriétés numériques de programmes séquentiels, tandis que mes recherches actuelles se tournent vers l'analyse de programmes concurrents, d'où le titre de ce mémoire. Les deux premiers chapitres de ce mémoire constituent une introduction, tandis que les suivants présentent mon travail d'habilitation proprement dit. Le premier chapitre est une introduction informelle à la problématique de l'analyse de programmes, aux méthodes existantes, leurs forces et leurs faiblesses. Le deuxième chapitre présente de manière formelle les outils dont nous aurons besoin par la suite : les bases de l'interprétation abstraite, quelques domaines abstraits existants et la construction d'analyses statiques par interprétation abstraite, ainsi que quelques résultats utiles que j'ai obtenu en doctorat. Le troisième chapitre est consacré aux aspects spécifiques de l'analyse de programmes concurrents. Cette recherche, très personnelle, a abouti à la construction d'une méthode d'analyse de programmes concurrents, paramétrée par le choix de domaines abstraits, et basée sur une notion d'interférence abstrayant les interactions entre threads. Ainsi, l'analyse construite est modulaire pour les threads. Cette méthode est reliée aux preuves rely-guarantee proposées par Jones, ce que nous montrons formellement dans une première partie. Nous construisons ensuite une analyse à grands pas basée sur les interférences, efficace et facile à implanter. Les deux dernière parties étudient les liens entre l'analyse et les modèles mémoires faiblement cohérents (désormais incontournables) ainsi que le raffinement de l'analyse pour tenir compte des propriétés spécifiques des ordonnanceurs temps-réels (nous étudions en particulier l'effet des priorités des threads et l'emploi d'objets de synchronisation). Le quatrième et le cinquième chapitres sont consacrés à la constructions de domaines abstraits. Ceux-ci ne sont pas spécifiquement liés au problème de la concurrence ; ils sont utiles à l'analyse de tous programmes, séquentiels comme concurrents. Le chapitre 4 étudie des domaines numériques inférant des égalités et inégalités affines, développés en collaboration avec Liqian Chen, alors doctorant en visite à l'ENS. La motivation première était l'emploi de nombres à virgule flottante afin d'améliorer l'efficacité du domaine des polyèdres, mais ces travaux ont également débouché sur la découverte de nouveaux domaines, basés sur les relations affines à coefficients intervalles, que nous présentons également. Le chapitre 5 étudie les abstractions de types de données réalistes, comme ceux rencontrés dans le langage C : les entiers machines, les nombres à virgule flottante, et les blocs structurés (tableaux, structures, unions). Nos abstractions modélisent finement les détails de l'encodage en mémoire des données afin de permettre l'analyse de programmes qui en dépendent (par exemple, ceux utilisant le type-punning). Ces abstractions sont motivées par nos expériences d'analyses, avec les outils Astrée et AstréeA, de programmes C industriels ; ceux-ci employant fréquemment ce type de constructions de bas niveau. Le sixième chapitre est consacré aux applications des méthodes présentées ci-dessus à la construction d'outils d'analyse statique. Il décrit en particulier mon travail sur l'outil Astrée que j'ai co-développé avec l'équipe Abstraction pendant et après mon doctorat, et qui a été industrialisé en 2009. Mes résultats théoriques et appliqués ont contribué au succès d'Astrée, tandis que celui-ci m'a fourni de nouveaux thèmes de recherches, sous la forme de problèmes concrets dont la résolution n'a pu se faire que grâce à des développements théoriques. Ce chapitre décrit également AstréeA, une extension d'Astrée utilisant l'abstraction d'interférences proposée plus haut pour l'analyse de programmes concurrents (Astrée étant limité aux programmes séquentiels). Il décrit également Apron, une bibliothèque de domaines abstraits numériques que j'ai co-développée. Il s'agit d'un outil plus académique, dont le but est d'encourager la recherche sur les domaines numériques abstraits. Le mémoire se conclue par quelques perspectives sur des recherches futures.

27 pages; In this article, we present a model and a denotational semantics for hybrid systems made of a continuous and a discrete subsystem. Our model is designed so that it may be easily used for modeling large, existing, critical embedded applications, which is a first step toward their validation. The discrete subsystem is modeled by a program written in an extension of an imperative language and the continuous subsystem is modeled by differential equations. We give to both subsystems a denotational semantics inspired by what is usually done for the semantics of computer programs and then we show how the semantics of the whole system is deduced from the semantics of its two components. The semantics of the continuous system is computed as the fix-point of a modified Picard operator which increases the information content at each step. This fix-point is computed as the supremum of a sequence of approximations and we show that this supremum exists and is the solution of a differential equation using Keye Martin's measurement theory. The semantics of the discrete system is given as a classical denotational semantics, except that special denotations are given for the actions of sensors and/or actuators.

This paper reports on the implementation of a pilot program aimed at improving student writing in a intermediate macroeconomics course. The Program attempted to reduce what is labelled the expectations gap between student and academic perceptions of what constitutes "good writing". This was done in two ways, Firstly, a range of resources designed to describe the characteristics of good writing was provided to students who were helped to structure their writing according to these characteristics. A series of academic literacy workshops formed the centerpiece of this strategy. Secondly, markers themselves were briefed on these characteristics and an approach to marking based upon them was negotiated. The impact of this program on student writing was very promising. Students who attended the academic literacy workshops performed better in the first of two written assignments than those who did not, controlling for general ability. These students were less likely to fail and more likely to be awarded a grade at Distinction level or above. The paper also identifies a number of important areas that need to be developed at the next stage of implementation including better integration of published writing huidelines and sample papers into the workshop curriculum, and collection of more qualitative data to suppliment the quantitative evaluations the paper offers.