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 ...
Voir