Until July 6, an international research event is taking place in Nancy with world experts in logic and automatic reasoning. An opportunity to explain this discipline between mathematics and computer science.
It is an international scientific event, organized by scientists from INRIA, which takes place until July 6 in Nancy. World experts in logic and automatic reasoning are present at the Institute of Digital Sciences, Management Cognition (IDMC).
The opportunity to take an interest in an exciting field of research that has concrete applications in our daily lives. We asked Stephan Merz, INRIA research director and head of the Veridis team.
It is a discipline between mathematics and computer science.It provides essential tools to solve complex problems in a methodical and rigorous manner.“, says Stephan 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 calculus, mathematics or geometry, we use theorems and deductions, therefore logical strategies. Automated reasoning uses computers, which use the same tools to solve complex problems.
Logic and automatic reasoning have various applications in different fields.It is easy to imagine, in the field of aviation or trains, the need for certification before software is put into service. It is important to guarantee certain correctness properties, for example that two trains never occupy the same section of track, that the metro stops in front of the gantries, or that two planes always keep 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 very sophisticated and automated techniques for these critical systems.“, explains the INRIA research director.
The same techniques are used in systems with high financial stakes, for example in the online storage and processing system, the cloud. Companies need to guarantee 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 is used to check the validity of programs. It could be used in the context of the autonomous car to guarantee safety systems controlling avoidance.
A growing number of software companies are using specialists in formal methods to verify by computer, in particular using automatic reasoning techniques, the correct functioning of critical computer components. The reason: any anomaly could have dramatic consequences.
“Some automatic deduction experts work for GAFAM or for the space agencies NASA or ESA” says Stephan Merz.
This year 2024, the city of Nancy has been selected 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.
The organization of such a conference is crucial to continue to make Nancy a strong place in formal methods, in the verification of complex systems and in automatic reasoning.
Workshops and conferences are being organized until July 6 at the Institute of Digital Sciences, Management Cognition (IDMC) in Nancy.
