Sites Inria

There are 4 Results with the keyword : "Proof of programs"


Coq takes the ACM Software System Award


The ACM (Association for Computing Machinery) recently announced the selection of the Coq development team for the "Software System Award".  This prize rewards a long-term group effort, which Inria has been supporting for some 30 years.


Home > News > News from Inria > Coq récompensé par l’ACM Software System Award


Claude Marché, Toccata team leader - © Inria / Photo Kaksonen


When programs prove themselves

Emmanuelle Perrot - 18/10/2013

In 2013, eight years after the creation of the Proval team headed by Christine Paulin-Mohring, the team has reached a turning point. Today it has taken on new directions and a new manager, Claude Marché. Claude tells us more about this new team, Toccata.


Home > Centre > Saclay > News > Quand les programmes font leurs preuves


Claude Marché, Toccata team leader - © Inria / Photo Kaksonen

Research-Industry partnership

ProofInUse: a joint Inria and AdaCore laboratory

Bertrand Bourgine - 17/03/2014

With the launch of a joint laboratory, the Toccata research team, which specialises in formal specification and computer-assisted proofs, is increasing its collaboration with AdaCore, the specialist publisher of development software for critical systems.


Home > Centre > Saclay > News > ProofInUse : le LabCom Inria-AdaCore


© Inria / Photo Kaksonen

European Research Council 2011

Dale Miller: “Making proof universal”

Sophy Caulier - 9/01/2012

As the beneficiary of an ERC Advanced Grant for experienced researchers, Dale Miller has embarked on the difficult path of establishing proof. His aim? In this field, which is highly abstract but which has a definite impact on the real world, he wishes to standardise proof systems and issue certificates for such systems in order to promote greater confidence in them.


Home > News > News from Inria > Dale Miller : Faire que la preuve soit universelle