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) annotated 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. For the annual research report, we are putting most of our publications on HAL. See the 2010 list here.
Defenses:
- Ph.D. defense of François Bobot on December 12th, 2011
- Ph.D. defense of Romain Bardou on October 14th, 2011
- Ph.D. defense of Stéphane Lescuyer on January 4th, 2011
- Habilitation defense of Xavier Urbain on November 29th, 2010
- Ph.D. defense of Johannes Kanig on November 26th, 2010
Arrivals (since September 2010):
- (2011/10) Denis Cousineau (new postdoc)
- (2011/10) Catherine Lelay (PhD student)
- (2011/10) Alain Mebsout (PhD student)
- (2011/05) Evgeny Makarov (new postdoc)
- (2011/05) Catherine Lelay (new intern)
- (2011/04) Cody Roux (new postdoc)
- (2011/04) Daisuke Ishii (invited researcher)
- (2011/01) Claire Dross (PhD student working part-time at Adacore)
- (2011/01) Nuno Gaspar (new intern)
- (2010/10) David Baelde (new postdoc)
- (2010/09) Véronique Benzaken (from the Database group)
- (2010/09) Kim Nguyen (new associate professor)
