Procédures de décision pour l'analyse de vulnérabilités

Formal methods have repeatedly demonstrated their relevance in search and analysis of bugs. If current methods are well suited to critical code analysis where mistakes are not a possible option, they are less interested on non-critical programs. Indeed, on such programs bugs are too numerous and only the most serious are corrected, a practice that does not fit well with today's tools.The aim of this thesis is therefore to allow such a gradation in the context of formal methods, which involves developing new decision procedures tailored to vulnerability analysis.Les méthodes formelles ont à plusieurs reprises montré leur pertinence dans la recherche et l'analyse de bogues. Si les méthodes actuelles sont bien adaptées à l'analyse de code critique où les erreurs ne sont pas une option, leur intérêt est moindre sur des programmes non critique. En effet, sur de tels programmes où les bugs sont pléthores, seuls les plus graves sont corrigés, une distinction qui ne sied pas avec les outils d'aujourd'hui.Le but de cette thèse est donc de permettre une telle gradation dans le contexte fort des méthodes formelles, ce qui passe par le développement de nouvelles procédures de décisions adaptées à l'analyse de vulnérabilité