TOCCATA

Toccata is a research group of the INRIA Saclay-Île-de-France research
center, joint with the Laboratoire Méthodes Formelles (Université-Paris-Saclay, CNRS, ENS)
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.