Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

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 (Frama-C/Jessie) and Java programs (Krakatoa) annotated with formulas describing the expected behavior, are constructed on top of this tool.

Click on the themes presented on the figure aside, or browse the "Research" item of the menu above, for detailed descriptions of the scientific activities the team. You can also find recent results described in our annual research report for 2011.

Defenses:

Arrivals (since September 2010):

INRIA Saclay - Île-de-France              Université Paris-sud              CNRS              LRI