European partnerships
Proof assistants: strengthening the position of the EU through EuroProofNet
Date:
Changed on 03/08/2022
Inria is leading EuroProofNet, an action launched by EU funding organisation COST, which addresses the safety and security of critical IT systems. IT researchers from the institute have joined forces with their counterparts from around thirty or so countries across Europe to improve the interoperability of proof assistants - a major issue for cybersecurity.
Uniting a community of researchers in Europe
Launched in November 2021, EuroProofNet is just reaching cruising speed as we begin the year. The aim of this action from EU funding organisation COST (European Cooperation in Science and Technology), directed by Frédéric Blanqui, a research fellow within Deducteam (a joint undertaking involving Inria Saclay, the ENS Paris-Saclay and Université Paris-Saclay) of the LMF ? To unite a community of researchers in Europe with an interest in the verification of software programs and digital proof systems, the goal being to improve the interoperability of different tools and to make their use easier in Europe and worldwide.
Frédéric Blanqui, the man behind the project, has brought together a broad scientific community made up of more than 200 participants, representing around thirty or so countries in Europe. EuroProofNet has been allocated a budget of €150k for its first year (it will run for a total of four years), and will hold networking events such as conferences, symposia, scientific visits, exchanges between researchers, etc.
Frédéric Blanqui - a brief bio
For more than 20 years Frédéric Blanqui has devoted himself to both practical and theoretical subjects in the field of IT: “type systems” and “rewriting systems”. Combining the two together is central to his research into proof systems. After graduating with a PhD from Orsay University in 2001 and continuing his research as a postdoctoral researcher at the University of Cambridge in 2002, he joined Inria in 2003, first at the site in Nancy, before moving to Paris and then finally Cachan and Saclay.
Five years spent in Beijing, as part of a team created within the LIAMA, the Sino-European Laboratory in Computer Science, gave him experience of working internationally, which will no doubt come in handy when coordinating the network of 220 researchers from across Europe as part of EuroProofNet.
The vital role played by proof assistants
This field of research is extremely important from a scientific and technological point of view, given how vital proof systems are when it comes to validating critical systems. These are used to ensure the smooth running of complex software programs employed in a range of sectors: in the aerospace industry (for space rocket guidance systems), in health (to make sure medical devices are reliable, in radiography, cardiology, etc.), banking (for the security of data management systems or transaction encryption), energy (for controlling nuclear power plants) and cybersecurity.
What is the purpose of verification? “A proof demonstrates the validity of a software program or an electronic system, which designers of critical applications seek to establish. Proof systems can be used to demonstrate that the software in question actually performs the task it was designed for and delivers the expected results”, explains Frédéric Blanqui.
Image
Verbatim
Proof assistants all operate by following their own individual computing and logic systems, but there can sometimes be incompatibilities between approaches employed by different tools
Auteur
Poste
Inria researcher in the Deducteam project-team
The researcher explains: “There are two types of proof systems. For simple problems, specific programs are capable of automatically detecting errors in code. However, their scope of action is limited, and for more complex problems, formal proofs of validity can be obtained ‘by hand’ using proof assistants”.
The EU - heavily invested in research
Alongside the USA, Europe is one of the world’s leading centres for research and development when it comes to proof assistants. European researchers are particularly active in this field, which is constantly changing as a result of demand. Software such as Coq, developed by Inria, or Isabelle, designed in the UK and Germany, are among those proof assistants most used by computer engineers, in addition to tools developed by other researchers.
Proof systems are based on a few axioms (statements considered to be universal), combined with reasoning rules, which are used to arrive at logical conclusions, like in mathematics. Software programs also use computer functions, which are available in libraries specific to the tool. “Proof assistants all operate by following their own individual computing and logic systems, but there can sometimes be incompatibilities between approaches employed by different tools”, explains Frédéric Blanqui.
The interoperability of proof assistants - a key concern
How can you be certain that the conclusions arrived at by a proof assistant regarding the validity or security of a program are reliable - i.e. that they are not dependent on the system being used? “We could, for example, carry out independent verification using different tools and reinforce trust in a proof system by testing its conclusions out on conclusions from other systems”, answers Frédéric Blanqui. “In order to do so, you need to be able to 'translate’ the features of one tool over to another.”
The interoperability of proof assistants is therefore central to EuroProofNet, which has a total of six working groups, each dedicated to a specific subject. Aside from the interoperability of proof assistants, there is also automated proving, software verification, the development of libraries of online proofs, the development of machine learning in proving, and research into type theory, which is used as a basis for modern proof assistants.
High scientific ambitions
Verbatim
The action will also have other outcomes, including strengthening the EU’s position from an academic and industrial perspective in what is a key emerging and economically dynamic market
Auteur
Poste
Inria researcher in the Deducteam project-team
“We began our initial discussions within the EuroProofNet network in early February, with a meeting held in Valencia in Spain, which was ‘hybrid’ as a result of the current situation”, explains Frédéric Blanqui. “Other meetings are set to be held this year, and there is also to be a summer school in Nantes in France, which will give us an opportunity to familiarise ourselves with Dedukti, a language developed within Inria, which can be used to encode different features of logic systems in a modular way.”
The scientific ambitions set by EuroProofNet are high: one aim is to develop translation tools for use between proof systems, while another is to agree on a European standard. “The action will also have other outcomes, including strengthening the EU’s position from an academic and industrial perspective in what is a key emerging and economically dynamic market”, concludes Frédéric Blanqui.
Deducteam project-team
A joint undertaking involving Inria and the ENS Paris-Saclay, Deducteam is made up of Gilles Dowek, head of the team, four permanent researchers (Bruno Barras, Frédéric Blanqui, Valentin Blot and Jean-Pierre Jouannaud) and more than a dozen non-permanent researchers. They explore applications of proof theory to the design of logical frameworks, deal with interoperability between proof systems (an area in which Deducteam is a world leader) and work on the construction of universal mathematics libraries. Deducteam engages regularly with the industrial sector, in the fields of IT (Clearsy, Nomadic-Labs, etc.) and energy (Mitsubishi), most notably in the context of collaborative research projects.
More information
- « Why join a COST Action ? », COST - European Cooperation in Science and Technology, 21/11/2018
- Les objectifs d’EuroProofNet, EuroProofNet.
- An example of a proof assistant, Coq. Video: “Coq: practical aspects of type theory” (in french), Yves Bertot, InriaChannel, YouTube, 7/1/2019