Proof in Use

Claude Marche
Claude Marché Director
Inria
Research Director, leader of the Toccata research team.
Yannick Moy
Yannick Moy co-director
AdaCore
Software engineer, technical leader of the SPARK technology.
Claire Dross
Claire Dross
AdaCore
Software engineer, specialist in proof technology.
Jean-Christophe Filliâtre
Jean-Christophe Filliâtre
CNRS
Researcher, main developer of the Why3 technology.
Johannes Kanig
Johannes Kanig
AdaCore
Software engineer, leading developer of the SPARK technology.
Andrei Paskevich
Andrei Paskevich
Université Paris-Sud 11
Teaching assistant, second main developer of the Why3 technology.
Sylvain Dailler
Sylvain Dailler
Inria
Research Engineer

Past members

Clément Fumex
Clément Fumex
Inria
Research Engineer
David Hauzar
David Hauzar
Inria
Research Engineer

About the Toccata research team

Part of INRIA Saclay and the Laboratoire de Recherche en Informatique (UMR Université Paris-Sud and CNRS). This team develops and distributes software for program proof. The Toccata team collaborated for nearly ten years with industry users of these tools, including Airbus, Dassault-Aviation, Gemalto.

About AdaCore

AdaCore is an international software engineering company based in France and the United States. AdaCore develops and distributes software for the development of critical systems, in particular the GNAT Pro development environment for the Ada programming language. As part of a long-term partnershuip, AdaCore has worked since 2008 with the Altran group on the SPARK proof technology.

Sponsors

AdaCore Altran CNRS Inria