Connaissez-vous cette discipline entre mathématiques et informatique qui révolutionne notre quotidien?

Jusqu’au 6 juillet, un événement international de recherche se tient à Nancy avec des experts mondiaux de la logique et du raisonnement automatique. Cet événement, organisé par des scientifiques de l’INRIA et de l’Université de Lorraine, se déroule à l’Institut des sciences du Digital, Management Cognition (IDMC). C’est l’occasion de découvrir cette discipline fascinante entre mathématiques et informatique.

Définition de la Discipline

Selon Stephan Merz, directeur de recherche INRIA et responsable de l’équipe Veridis, cette discipline permet de résoudre des problèmes complexes de manière méthodique et rigoureuse en utilisant des preuves mathématiques. Le raisonnement automatisé est un domaine de l’informatique qui tente de fournir des garanties sur le comportement des systèmes et des programmes, en s’appuyant sur des preuves mathématiques. Pour résoudre des problèmes logiques en calcul, en mathématiques ou en géométrie, des théorèmes et des stratégies logiques sont utilisés, et ces mêmes outils sont appliqués par des ordinateurs pour résoudre des problèmes complexes.

Applications Concrètes

Les applications de la logique et du raisonnement automatique sont nombreuses et variées. Par exemple, dans le domaine de l’aviation ou des trains, il est essentiel de garantir que les logiciels respectent certaines propriétés de sécurité, comme éviter que deux trains occupent le même tronçon de voie ou que le métro s’arrête correctement face aux portiques. Dans les systèmes financiers, comme le cloud ou les systèmes bancaires, ces techniques garantissent la disponibilité et la fiabilité des services.

En programmation, la logique est utilisée pour écrire et vérifier la validité des algorithmes et des programmes. Dans le cadre de la voiture autonome, le raisonnement automatique pourrait garantir les systèmes de sécurité pour éviter les collisions.

Lien avec le Monde Industriel

De plus en plus d’entreprises font appel à des spécialistes en méthodes formelles pour vérifier par ordinateur le bon fonctionnement de composants informatiques critiques. Des experts en déduction automatique travaillent pour des géants comme les GAFAM ou pour des agences spatiales comme la NASA ou l’ESA.

La Conférence à Nancy

En 2024, Nancy accueille cet événement international, organisé par des scientifiques du centre Inria et de l’Université de Lorraine. Les équipes de recherche locales sont à la pointe des travaux en méthodes formelles et en vérification de systèmes complexes. L’organisation de cette conférence est cruciale pour renforcer la position de Nancy dans ce domaine.

Des ateliers et des conférences se tiennent jusqu’au 6 juillet à l’Institut des sciences du Digital, Management Cognition (IDMC) à Nancy.