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.
News
- The book Introduction à la science informatique edited by Gilles Dowek has been published by the CRDP Académie de Paris on July 2011 and is available at Amazon and Decitre.
- The paper Canonized Rewriting and Ground AC Completion Modulo Shostak Theories by Sylvain, Evelyne and Mohamed got the EATCS Award for Best ETAPs Paper 2011.
New releases:
- (Dec. 22th 2010) The first public release of Why3 is available
- (Dec. 17th 2010) Why 2.28 is available together with a version of the Jessie plug-in compatible with Frama-C version Carbon
Defenses:
- 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
For the annual research report, we are putting most of our publications on HAL. See the 2010 list here.
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)
