Abstract EN:

Cette thèse s'intéresse à divers aspects quantitatifs de l'analyse statique de programmes, notamment à la précision des analyses et aux analyses de consommation de ressources. Nous quantifions la précision des analyses numériques fondées sur la théorie de l'interprétation abstraite à l'aide de la théorie de la mesure. Nous examinons la théorie de l'interprétation abstraite probabiliste et la précision naturellement issue de la norme sur un espace de Hilbert. Nous proposons un cadre, nommé analyse statique quantitative qui partage avec cette dernière théorie le fait de modéliser les programmes par des opérateurs linéaires. Ce cadre permet d'exprimer d'une façon générique des consommations de ressources par un programme, grâce à une structure de dioïde, et de calculer des sur-approximations de ces consommations. Nous proposons notamment le concept de coût à long terme d'un programme, qui caractérise une consommation moyenne par pas d'exécution.