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

Nouvelles

Jean-Christophe Filliâtre co-organise VSTTE 2009 et PLPV 2010.

Un article de Sylvie Boldo, Guillaume Melquiond et Jean-Christophe Filliâtre a été accepté à la conférence Calculemus (Juillet 2009).

Un article de Sylvie Boldo a été accepté à la conférence ICALP (Juillet 2009).

En février 2009, Sylvie Boldo a publié un article à IEEE Transactions on Computers, dans la sections spéciale "arithmétique des ordinateurs".

En février 2009, nous accueillons une nouvelle doctorante, Tuyen Nguyen.

En janvier 2009, début des projets ANR Fost et U3CAT.

En septembre 2008, début du projet Hisseo, financé par Digiteo.

En novembre 2008, nous accueillons Guillaume Melquiond comme nouveau chargé de recherche INRIA .

Un article de vulgarisation scientifique sur la programmation vient de paraître dans le dernier numéro de DocSciences (novembre 2008), écrit par Sylvie Boldo.