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

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:
- Ph.D. defense of Thi Minh Tuyen Nguyen on June 11th, 2012
- Ph.D. defense of François Bobot on December 12th, 2011
- Habilitation defense of Jean-Christophe Filliâtre on December 2nd, 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 (postdoc)
- (2011/10) Catherine Lelay (PhD student)
- (2011/10) Alain Mebsout (PhD student)
- (2011/05) Evgeny Makarov (postdoc)
- (2011/05) Catherine Lelay (intern)
- (2011/04) Cody Roux (postdoc)
- (2011/04) Daisuke Ishii (invited researcher)
- (2011/01) Claire Dross (PhD student working part-time at Adacore)
- (2011/01) Nuno Gaspar (intern)
- (2010/10) David Baelde (postdoc)
- (2010/09) Véronique Benzaken (from the Database group)
- (2010/09) Kim Nguyen (associate professor)