PROVAL Research team
Proofs of programs
- Leader : Christine Paulin
- Research center(s) : Saclay - Île-de-France
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Programs, Verification and Proofs
- Université Paris-Sud (Paris 11), CNRS, Laboratoire de recherche en informatique (LRI) (UMR8623)
Team presentationThe objective of the ProVal research project-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.
This project stems from project LogiCal. It is based on the formalism of type theory which provides a clear semantic framework to represent proofs and computations in the machine.
The project develops a generic program proof environment (Why), 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) and Java programs (Krakatoa) annoted with formulas describing the expected behavior, are constructed on top of this tool. The projects is also specialized in proving the behavior of computations involving floating-point numbers.
Program proof models and methods.
We develop models for programming languages and specification languages that meet the needs of critical applications and are adapted to interactive or automatic proof. We are interested in particular in the modeling of abstract constructs of higher order, pointer manipulation and floating-point arithmetic.
Architecture of program proof environments.
The implementation of our methods into tools poses scaling problems in the generation of proof demands, annotation writing methodology problems, specification language expressivity problems, and specification development aid problems.
Program proof requires an adaptation and specialization of general provers. The project studies especially termination proofs, as well as the combination of decision procedures. Special attention is paid to the correctness of such techniques.
The techniques developed within the project have applications in the fields that necessitate the development of critical sofware, for which certification needs are high. This concerns especially the bank, aeronautics and telecommunication sectors. We are aiming at the certification of embedded C or Java code, as well as the certification of code generation tools.