Cette dernière décennie a vu l'essor des analyses statiques plus seulement réservées aux systèmes embarqués critiques (avions, métros, fusées, etc.), mais maintenant disponibles plus largement, comme le montre l'implication de compagnies telles que Google ou Facebook dans le domaine.

Néanmoins, prouver l'absence de bugs d'un logiciel, (problème que nous savons depuis Turing et Cook être intrinsèquement difficile) n'est pas le seul challenge en développement logiciel. En effet, la complexité toujours croissante des logiciels induit un besoin toujours croissant d'optimisations fiables.

La résolution de ces deux problèmes (fiabilité, optimisation) impose le développement de méthodes d'analyse statique sûres (sans faux négatifs), efficaces (en temps et en mémoire), mais suffisamment précises (avec un taux faible de faux positifs). La recherche de tels compromis est au coeur de mes travaux, qu'ils s'appliquent à la vérification formelle ou au domaine plus contraint des analyses pour les compilateurs.

Les travaux détaillés dans ce manuscrit décrivent mes activités de recherche pendant la période de 2009 à 2017. Durant cette période, j'ai contribué aux développements d'analyses statiques appliquées aux deux domaines connexes que sont la vérification de logiciels et la compilation. Les analyses proposées sont développées dans le cadre de l'interprétation abstraite, pour des domaines numériques, et plus récemment, des domaines mémoire. Elles font de plus l'objet de validation expérimentale en terme de précision et de coût, ainsi que de leur impact dans des analyses clientes (terminaison, optimisations) lorsque cela est pertinent.

Mots-clefs: Analyse statique, vérification de logiciel, compilation, optimisation de code, domaines numériques, domaine mémoire, terminaison.

This last decade was the occasion to see the rise of static analyses that are now no longer reserved for critical embedded systems (airplanes, subways, rockets, etc.). They are now more widely available, as evidenced by the novel implication of companies like Google or Facebook in the domain.

Nevertheless, proving the absence of bugs in a given software (problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations.

Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers). Finding such compromises is the core of my works, whether it deals with formal verification or the more specific domain of analyses inside compilers.

The work which is detailed in this manuscript was done over a period going from 2009 to 2017. During this period, I contributed to static analyses in the two related domains that are software verification and compilation. The proposed analyses have been developed within the abstract interpretation framework, for numerical domains, or, more recently, memory domains. They are also experimentally validated, according to precision and cost criteria, and also according to their impact on client analyses (termination, code optimisation) whenever appropriate.

Keywords: Static Analysis, Software Verification, Compilation, Code Optimisation, Numerical Domains, Memory Domains, Termination.