Habilitation

J'ai soutenu mon Habilitation intitulée:

le :

en :

devant le jury composé de:

Résumé

De nombreux programmes sont désormais concurrents, y compris dans le monde des logiciels embarqués critiques, comme ceux de l'industrie avionique. Ces programmes sont notamment difficiles à concevoir et à vérifier. Dans ce travail, nous proposons une méthode d'analyse statique permettant de s'assurer de leur sûreté. Les analyses statiques s'exécutent à la compilation et sont automatiques. Elles sont approchées, ce qui est nécessaire à leur efficacité. Elles sont néanmoins sûres et emploient des sûr-approximations afin d'inférer des propriétés vraies de toutes les exécutions du programme analysé et de ne pas oublier d'erreur. Notre cadre de travail est celui de l'interprétation abstraite, une théorie générale de l'approximation des sémantiques de programmes. La méthode que nous proposons est modulaire (par processus) et paramétrée par un choix de domaines abstraits, permettant ainsi de contrôler la balance entre le coût et la précision et d'adapter l'analyse à des programmes cibles.

Dans une première partie nous présenterons un résultat fondamental : la formalisation par interprétation abstraite d'une version constructive de la méthode de preuve "rely-guarantee" proposée par Jones. Ceci ouvre la voie vers l'inférence automatique et modulaire d'invariants. Nous construisons ensuite une analyse statique de programmes concurrents par abstraction de cette sémantique. L'analyse est paramétrée et peut facilement exploiter les techniques et abstractions développées pour l'analyse de programmes séquentiels. Nous présenterons des techniques de partitionnement par l'état de l'ordonnanceur, permettant de tenir compte des primitives de synchronisation (comme les verrous et les priorités). Nous évoquerons également la sûreté l'analyse dans les modèles de mémoires faiblement cohérentes, utilisées par les architectures modernes. La dernière partie de l'exposé présentera AstréeA, un prototype d'analyseur statique basé sur Astrée, et donnera quelques résultats expérimentaux sur l'analyse d'un logiciel embarqué critique industriel de grande taille.

Mémoire

Mémoire.

Le format du mémoire ci-dessus est compact, afin de réduire le nombre de pages (deux colonnes, marges petites, 9 points). Une version avec des polices plus grosses (et une colonne) est également disponible. Ces mémoires emploient une coloration syntaxique. Si vous souhaitez imprimer le mémoire, il existe également une version noir & blanc compacte et une version noir & blanc avec grosses polices.

Exposé

Transparents de l'exposé.