La quinzaine internationale de la logique et du raisonnement automatique se tiendra à Nancy !

Du 26 au 29 juin se déroulera l'école d'été "Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR)" au Centre Inria de l'Université de Lorraine à Villers-Lès-Nancy. Elle sera suivie par la conférence internationale "International Joint Conference on Automated Reasoning" (IJCAR) du 1er au 6 juillet à l'IDMC. Plongez au cœur de cet événement international de recherche grâce à l'interview de Sophie Tourret (Inria), Stephan Merz (Inria), Didier Galmiche (Université de Lorraine) et Christophe Ringeissen (Inria), les membres du comité d'organisation.

Sur quel domaine porte la conférence IJCAR ?

La conférence IJCAR est centrée sur la conception de prouveurs de théorèmes qui sont des outils informatiques capables d'effectuer plus ou moins automatiquement des démonstrations mathématiques. C'est une thématique de recherche à l'interface entre mathématiques et informatique, correspondant à une forme d'intelligence artificielle symbolique. La conception de prouveurs de théorèmes repose sur l'étude approfondie d'une grande variété de logiques et de calculs permettant de modéliser et de mécaniser différents aspects du raisonnement.

La problématique sous-jacente à ce domaine de recherche devrait facilement trouver un écho auprès du plus grand nombre !

Quel élève ou quel étudiant n'a pas été confronté à effectuer une preuve d'une propriété mathématique, en se disant que ce serait génial d'avoir un outil informatique pour (l'aider à) la faire ? 

À long terme, l'un des objectifs de la communauté fédérée par IJCAR est de pouvoir proposer des prouveurs de théorèmes utilisables par le plus grand nombre et pas seulement par les spécialistes du domaine.

Quelles sont les applications concrètes ?

Les techniques et méthodes développées dans le domaine du raisonnement automatique permettent d'effectuer à l'aide d'un ordinateur des preuves de propriétés. D'un point de vue mathématique, une propriété peut être considérée comme un théorème à démontrer formellement. D'un point vue logiciel, nous pouvons par exemple chercher à montrer la propriété qu'un programme termine toujours. Les techniques de preuve peuvent apporter un niveau de confiance que le test de logiciels est incapable de fournir. Elles sont par exemple utilisées dans les domaines du ferroviaire ou de l'avionique pour garantir des propriétés de sûreté, par les fournisseurs de services cloud qui doivent se prémunir de pannes qui conduiraient à l'indisponibilité de ces services, assorties de pénalités financières, ou encore en sécurité informatique pour démontrer l'absence de certaines attaques.

Si l'on reprend l'exemple des domaines du ferroviaire et de l’avionique, l'utilisation des méthodes formelles permet de démontrer que deux trains ne peuvent jamais occuper un même tronçon de voie, que le métro s’arrête en face des portiques, que deux avions gardent toujours une distance minimale etc.

Quels objectifs de ce rassemblement ?

L'objectif premier de la conférence est de contribuer à faire avancer la science dans le domaine du raisonnement automatique, par l'organisation d'un forum propice à l'échange des idées sur cette thématique.

 IJCAR est l’événement bisannuel incontournable dans le domaine du raisonnement automatique, où sont présentées les dernières avancées dans cette thématique essentielle dans le contexte de l’intelligence artificielle symbolique. 

IJCAR offre la possibilité de rencontrer les plus grandes et grands spécialistes du domaine. Les équipes de recherche de l'Université de Lorraine et du Centre Inria sont à la pointe des travaux scientifiques menés dans ce domaine. L'organisation d'une telle conférence nous paraît déterminante pour continuer de faire de Nancy une place forte en méthodes formelles, en vérification de système complexes et en raisonnement automatique. En montrant les très bonnes conditions de travail localement à l’Université de Lorraine, au Centre Inria, ainsi que le cadre de vie nancéien, nous pouvons estimer attirer à Nancy de nouveaux jeunes talents ou des chercheuses et chercheurs confirmés de renommée internationale.

Quels sont les liens avec les entreprises ?

Un nombre croissant d'entreprises développant du logiciel font appel à des spécialistes en méthodes formelles pour vérifier par ordinateur, notamment grâce à des techniques de raisonnement automatique, le bon fonctionnement de composants informatiques critiques pour lesquels une quelconque anomalie pourrait avoir des conséquences dramatiques. Ainsi la communauté d'IJCAR comprend des experts en déduction automatique travaillant pour les GAFAM et pour des agences comme la NASA.

Quels seront les temps forts ?

Plusieurs événements viendront ponctuer ces séquences autour de la logique et du raisonnement automatique : 

• l'école d'été SAT/SMT/AR organisée à Nancy dans la semaine précédant IJCAR permettra de compléter la formation des étudiants du domaine grâce à des cours de très haut niveau donnés par les plus grands spécialistes.
   
• une dizaine d'ateliers (workshops) se focalisant sur les travaux en cours dans des thématiques spécifiques
   
• un programme riche de 45 présentations sélectionnées par le comité de programme d'IJCAR
   
• trois orateurs invités de renommée internationale
   
• remise du prix Herbrand à Armin Biere. Le prix Herbrand est décerné chaque année à une sommité pour ses contributions au domaine du raisonnement automatique. Pour 2024, le prix Herbrand est décerné à Armin Biere, qui est l'un des plus grands spécialistes de la conception de solveurs pour la satisfiabilité propositionnelle (SAT)
   
• célébration du trentième anniversaire de la compétition CASC qui permet d'évaluer annuellement les performances des différents prouveurs de théorèmes développés à travers le monde. La compétition CASC a été lancée lors de la douzième édition de la conférence internationale sur le déduction automatique (CADE) ayant eu lieu en 1994 à Nancy. IJCAR 2024 représente donc un retour aux sources pour CASC