Section: Overall Objectives

Introduction

Critical software applications in the domain of transportation, telecommunication or electronic transactions are put on the market within very short delays. In order to guarantee a dependable behavior, it is mandatory for a large part of the validation of the system to be done in a mechanical way.

The ProVal team addresses this question and consequently participates to the INRIA major scientific priorities: “Programming: Security and Reliability of Computing Systems”.

Our approach uses Type Theory as a theoretical basis, a formalism which gives a clear semantics for representing, on a computer, both computation and deduction.

Type theory is a natural formalism for the specification and proof of higher-order functional programs, but we also use it as the kernel for deductive verification of imperative programs. It serves as a support for modeling activities (e.g. pointer programs, random computations, floating-point arithmetic, semantics).

Verification conditions (VCs) generated from programs annotated with specifications can often be expressed in simple formalisms (fragments of first-order logic) and consequently be solved using automated deduction. Building specialized tools for solving VCs, integrating different proof technologies, in particular interactive and automated ones, are important activities in our group.

When sophisticated tools are used for analyzing safety-critical code, their reliability is an important question: in an industrial setting, there is often a certification process. This certification is based on an informal satisfaction of development rules. We believe that decision procedures, compilers or verification condition generators (VCGs) should not act as black boxes but should be themselves specified and proved, or should produce evidence of the correctness of their output. This choice is influential in the design of our tools and is also a good challenge for them.

The project develops a generic environment (Why) for proving programs. Why generates sufficient conditions for a program to meet its expected behavior, that can be solved using interactive or automatic provers. On top of this tool, we have built dedicated environments for proving C (Frama-C/Jessie) or Java (Krakatoa) programs.

With the arrival of Sylvie Boldo in 2005 and Guillaume Melquiond in 2008 as junior researchers, the team is developing a strong expertise in the area of formal verification of floating-point arithmetic.

Our research activities are detailed further, following the three themes:

• Interactive proofs of programs,

• Proof of imperative and object-oriented programs,

• Automated deduction for program proof.

Development of tools and applications is an important transversal activity for these four themes.