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.