Overview
ProVal is a project-team of the INRIA Saclay - Īle-de-France research center, joint with LRI (CNRS and University of Paris Sud), located in Orsay, France.The objective of the team is to propose methods and tools that can be integrated into the software development cycle and that make it possible to produce code that is proven to be correct with respect to its expected behavior.
The team develops a generic program proof environment (the Why platform), that is able to generate proof demands that can then be delegated to automatic or interactive provers. Dedicated environments to prove C programs (Caduceus) and Java programs (Krakatoa) annoted with formulas describing the expected behavior, are constructed on top of this tool.
Detailed description of scientific activities are described in the annual research report.
News
Jean-Christophe Filliātre is co-organizing VSTTE 2009 and PLPV 2010.
An article by Sylvie Boldo, Guillaume Melquiond and Jean-Christophe Filliātre has been accepted for Calculemus (July 2009).
An article by Sylvie Boldo has been accepted for ICALP (July 2009).
In February 2009, Sylvie Boldo has published an article in IEEE Transactions on Computers, special section on Computer Arithmetic.
In February 2009, we welcome a new Ph.D. student, Tuyen Nguyen.
In January 2009, beginning of the ANR projects Fost and U3CAT.
In September 2008, beginning of the Hisseo project, funded by Digiteo.
In November 2008, we welcome Guillaume Melquiond as a new permanent INRIA researcher.
A popular science article about programmation can be found in the latest DocSciences (November 2008), written (in French) by Sylvie Boldo.