ORSAY oN d’ordre: 9366 UNIVERSITÉ DE PARIS-SUD 11 CENTRE D’ORSAY THÈSE présentée pour obtenir le grade de docteur en sciences DE L’UNIVERSITÉ PARIS XI PAR Yannick MOY ! SUJET : Preuve automatique et modulaire de la sûreté de fonctionnement des programmes C Automatic Modular Static Safety Checking for C Programs soutenue le 15 janvier 2009 devant la commission d’examen MM. Burkhart Wolff K. Rustan M. Leino Xavier Leroy Michael Norrish Claude Marché Pierre CrégutJ’ai commencé cette thèse, après quatre années à la R&D de PolySpace, parce que je voulais comprendre comment mieux répondre au problème d’analyse et de vérification des programmes informatiques. Ces trois années m’ont largement satisfaites sur ce point, et m’ont permis de connaître des personnes admirables autant du point de vue professionnel que personnel. Je voudrais remercier pour leur fantastique état d’esprit toutes les personnes de l’équipe ProVal, avec une mention spéciale à Évelyne et Jean-Christophe pour leurs gâteaux déli- cieux, et Jean-Christophe et Sylvain pour l’ambiance sonore chaleureuse. Je remercie respectueusement mes deux directeurs de thèse, Claude et Pierre, pour m’avoir accompagné ces trois années sur le dur chemin de la recherche, et je leur dis mon admiration pour leur talent et leur travail. Je veux remercier sincèrement toutes les personnes de mon jury en plus de mes di- recteurs, Burkhart, Rustan, Xavier et Michael, qui sont tous des chercheurs que j’admire profondément. Vos ...