Sites Inria

Version française

TOCCATA Research team

Certified Programs, Certified Tools, Certified Floating-Point Computations

Team presentation

Toccata is a research group of the INRIA Saclay-Île-de-France research
center, joint with the Laboratoire de Recherche en Informatique (CNRS
& University of Paris-Sud), part of the Université-Paris-Saclay
cluster, and located in Orsay, France.

The general objective of the team is to promote formal specification
and computer-assisted proof in the development of software that
requires a high assurance of its safety and its correctness with
respect to its intended behavior. We work on the design of methods and
tools for deductive verification of programs. One of our original
skills is the ability to conduct proofs by using automatic provers and
proof assistants at the same time, depending on the difficulty of the
program, and specifically the difficulty of each particular
verification condition. In particular in the context of the Why3
software environment, we want to provide methods and tools for
deductive program verification that can offer both a high amount of
proof automation and a high guarantee of validity. We develop our own
theorem prover, Alt-Ergo, not only used within Why3 but within other
external applications, and also within our own tool Cubicle dedicated
to concurrent programs.

In industrial applications, numerical calculations are very common
(e.g. control software in transportation). Typically they involve
floating-point numbers. Some of the members of Toccata have an
internationally recognized expertise on deductive program verification
involving floating-point computations. Our past work includes a new
approach for proving behavioral properties of numerical C programs
using Frama-C/Jessie, various case studies of applications of that
approach, the use of the Gappa solver for proving numerical
algorithms, and an approach to take architectures and compilers into
account when dealing with floating-point programs.  We also
contributed to the Handbook of Floating-Point Arithmetic.  A
representative case study is the analysis and the proof of both the
method error and the rounding error of a numerical analysis program
solving the one-dimension acoustic wave equation. Our experience led
us to a conclusion that verification of numerical programs can benefit
a lot from combining automatic and interactive theorem
proving. Verification of numerical programs is another main research
axis of Toccata.

Research themes

Our scientific programme in structured into four objectives:

* deductive program verification;

* automated reasoning;

* formalization and certification of languages, tools and systems;

* proof of numerical programs.

The details on each axis can be seen on our team web page and in our annual activity reports.

International and industrial relations

Our industrial transfer actions involve:

* The joint laboratory ProofInUse joint with SME AdaCore, for the
development of the SPARK toolset for the verification of
safety-critical Ada programs

* The collaboration with the OCamlPro company for the industrial
transfer of the Alt-Ergo automated theorem prover

Keywords: Deductive Program Verification Automated Reasoning Formalization in Higher-Order Logics Numerical Programs.