Présentation
ProVal est une équipe-projet du centre de recherche INRIA
Saclay - Île-de-France, commune avec le LRI (CNRS et Université
Paris Sud), située à Orsay, France.
L'objectif de cette équipe est de proposer des méthodes et des outils pouvant s'intégrer dans le cycle de développement logiciel et permettant de produire du code correct vis-à-vis de comportements attendus.
L'équipe développe une plateforme générique de vérification de programmes (la platforme Why), qui produit des obligations de preuve à partir de programmes annotés de spécifications formelles et les transmet ensuite à des outils de preuve, interactifs ou automatiques. Des instances pour les langages C (Caduceus) et Java (Krakatoa) sont bâties sur cette infrastructure générique.
Une description détaillées des activités scientifiques de l'équipe se trouve dans le rapport annuel d'activité (en anglais). Pour le rapport annuel d'activités, nous mettons la plupart de nos publications sur HAL. Voir la liste 2010 ici.
Soutenances :
- de thèse de François Bobot le 12 décembre 2011
- de thèse de Romain Bardou le 14 octobre 2011
- de thèse de Stéphane Lescuyer le 4 janvier 2010
- d'HDR de Xavier Urbain le 29 novembre 2010
- de thèse de Johannes Kanig le 26 novembre 2010
Arrivées (depuis septembre 2010) :
- (2011/10) Denis Cousineau (nouveau postdoctorant)
- (2011/10) Catherine Lelay (doctorante)
- (2011/10) Alain Mebsout (doctorant)
- (2011/05) Evgeny Makarov (nouveau postdoctorant)
- (2011/05) Catherine Lelay (nouveau stagiaire)
- (2011/04) Cody Roux (nouveau postdoctorant)
- (2011/04) Daisuke Ishii (chercheur invité)
- (2011/01) Claire Dross (doctorante en collaboration avec Adacore)
- (2011/01) Nuno Gaspar (nouveau stagiaire)
- (2010/10) David Baelde (nouveau postdoctorant)
- (2010/09) Véronique Benzaken (du groupe Base de Données)
- (2010/09) Kim Nguyen (nouveau maître de conférences)
