Wiki Agenda Contact Version française


topics floating-point computation automated deduction interactive theorem proving proof of programs data-centric languages synchronous programming

Toccata is a research team of the INRIA Saclay - Île-de-France research center, joint with LRI (CNRS and University of Paris-Sud), located in Orsay, France. It was created in September 2012, partly as a refoundation of the former team ProVal. Members of Toccata are also members of the VALS group of LRI.

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.

Click on the themes presented on the figure aside, or browse the "Research" item of the menu above, for detailed descriptions of the scientific activities the team. You can also find recent results described in the annual research report of the team in 2014.


[Conference] November 3-6, 2015
The 17h International Conference on Formal Engineering Methods takes place in Paris.
[Award] April 16th, 2015
Jean-Christophe Filliâtre and Guillaume Melquiond receive the "Best team" award of the VerifyThis@ETAPS2015 verification competition. Why3 also receives the "Distinguished user-assistance tool feature" award.
[Workshop] March 13th, 2015
The Frama-C day takes place at CEA Nano-innov in Saclay.
[Workshop] Feb 2, 2015
The ProofInUse KickOff takes place at Hotel Montparnasse, Paris.
[Arrival] Jan. 1, 2015
David Hauzar, new engineer working on the ProofInUse project
[Arrivals] Nov. 1, 2014
Clément Fumex, new engineer working on the ProofInUse project. Jacques Charles Mbiada Ndjanda, new PhD student supervised by C. Marché and J. Signoles (CEA List)
[Seminar] Oct 7, 2014
Digiteo Seminar "Desperately Needed Remedies for the Undebuggability of Large Floating-Point Computations in Science and Engineering" by W. Kahan.
[Visit] Oct. 6-7, 2014
Visit of Prof. William Kahan, Professeur University of California at Berkeley (Turing Award 1989).
[Defense] Oct. 6, 2014
Habilitation defense of Sylvie Boldo, amphi bat. 660, Univ. Paris-Sud.
[Defense] Sep. 29, 2014
Thesis defense of Alain Mebsout, batiment 650, Univ. Paris-Sud.
[Publication] Sep. 11, 2014
New book (in French) "Apprendre à Programmer avec OCaml" written by Sylvain Conchon and Jean-Christophe Filliâtre.
[Arrival] Sep. 1, 2014
Andrew Tolmach (Portland State University, USA) starts a 1-year visitor, funded by a Digiteo Chair
Older news

INRIA Saclay - Île-de-France              Université Paris-sud              CNRS              LRI