Des logiques formelles aux applications dans les mondes scientifiques et industriels
Colloquium LIRMM – Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Jeudi 2 juin 2022 de 14h à 16h, UM amphi Saint-Priest, entrée libre
(campus St-Priest bâtiment 2, 860 rue de St-Priest, Montpellier)
Gérard Berry , Informaticien, Professeur honoraire au Collège de France (chaire “Algorithmes, machines et langages” 2007–2019, détails @ CdF), membre de l’Académie des Sciences
Résumé :
Longtemps, la logique formelle a été considérée comme seulement un soubassement des mathématiques, pas vraiment utile en pratique. Mais ses progrès durant les 30 dernières années ont conduit à des applications entièrement nouvelles et de grande importance. Nous en détaillerons deux cas assez différents : celui des logiques finies comme le calcul booléen pur et le booléen modulo théories décidables, et l’utilisation d’assistants de preuve.
Pour les logiques finies, le calcul booléen, qu’on pensait insoluble même à des échelles moyennes, a connu deux révolutions. D’abord celle des diagrammes de décision binaires (BDDs), puis celle de la satisfaction Booléen (SAT), avec des applications depuis rendre trivial le Sudoku, jusque vérifier systématiquement des propriétés-clés des designs de circuits électroniques ou résoudre des problèmes combinatoires en théorie des nombres. Puis l’extension de SAT vers des théories décidables (SMT) a conduit à un spectre plus large d’applications, allant de la vérification d’applications dont la sûreté et la sécurité sont critiques à l’étude de certains systèmes biologiques.
Dans le domaines plus vaste des logiques d’ordre supérieur, des assistants de preuve comme HOL, Isabelle, Coq et Lean permettent maintenant des vérifications de la preuve formelle de grands théorèmes mathématiques (4-couleurs, Feit-Thompson, Kepler, etc), mais aussi des applications informatiques importantes en pratique comme la vérification formelle du compilateur C CompCert ou celle de cœurs de systèmes d’exploitation, entreprises impensables encore récemment.
Nous terminerons par quelques réflexions sur la convergence des méthodes finies et des assistants de preuve, qui sera nécessaire dans l’avenir.
Contact LIRMM : Virginie Fèche (Responsable Communication LIRMM)