Science. Do you know this major between mathematics and computer science that is revolutionizing our daily lives?

Until July 6, an international research event with world experts in logic and spontaneous reasoning will take place in Nancy. The opportunity to explain this discipline between mathematics and computer science.

It is an international scientific event organized by INRIA scientists and takes place until July 6 in Nancy. World experts in logic and automatic reasoning are present at the Institute of Digital Sciences and Management Cognition (IDMC).

The opportunity to take an interest in an exciting research area that has concrete applications in our everyday lives. We put the question to Stefan Merz, INRIA Research Director and Veridis Team Leader.

It is a major between mathematics and computer science.It provides the essential tools to solve complex problems in a systematic and rigorous manner.“,” explains Stefan Merz.
Automated reasoning is the field of computer science that attempts to provide guarantees about what a system or program will or will never do. This assurance is based on mathematical proofs.
To solve logical problems in arithmetic, mathematics, or geometry, we use theories and deductions, and therefore logical strategies. Automated reasoning uses computers, which use the same tools to solve complex problems.

Logic and automatic reasoning have diverse applications in different fields.It is easy to imagine, in the field of aviation or trains, the need for certification before software can be put into service. It is important to ensure certain corrective properties, for example that two trains never occupy the same section of track, or that a metro stops in front of bridges, or that two planes always maintain a minimum distance. At the most demanding level of these certifications, it is recommended to use these formal proof techniques to guarantee these properties. We need these sophisticated and highly automated techniques for these critical systems.“It is a great honour for me to be a part of this project,” explains INRIA’s Research Director.

The same techniques are used in systems with high financial risks, for example in online storage and processing systems, the cloud. Companies need to ensure the availability of their services, which is also useful for banking systems.

In programming, logic is used to write algorithms and computer programs. Automatic reasoning makes it possible to verify the correctness of programs. It can be used as part of a self-driving car to ensure safety systems that control avoidance.

An increasing number of software development companies are using specialists in formal computer verification methods, especially using automatic heuristics, to verify the proper functioning of important computer components. The reason: any anomaly can lead to serious consequences.

“Some of the automatic inference experts work for GAFAM or for space agencies NASA or ESA.“It's a very good idea,” says Stefan Merz.

This year, 2024, the city of Nancy has been chosen to host this international event. It is organized by scientists from the Inria Center and the University of Lorraine. The research teams from the University of Lorraine and the Inria Center are at the forefront of scientific work carried out in this field.

Organizing such a conference is crucial in continuing to make Nancy a strong place in formal methods, complex systems verification, and spontaneous reasoning.

Workshops and conferences are organized until July 6 at the Institute of Digital Sciences and Management Cognition (IDMC) in Nancy.