Prochain Colloquium du LIRMM – Gérard Berry – 2 juin 2022

Jeudi 2 juin à partir de 14h, nous aurons le plaisir d’accueillir Gérard Berry, éminent informaticien, ancien élève de l’École polytechnique, ingénieur général du corps des Mines, membre de l’Académie des sciences, de l’Académie des technologies et de l’Academia Europaea. Il viendra nous parler de logiques formelles aux applications dans les mondes scientifiques et industriels.
Rendrez pour ce prochain colloquium sur notre Campus, dans l’amphi St Priest afin de partager ce moment de science et de convivialité.
Biographie : https://www.college-de-france.fr/site/gerard-berry/
Sujet : Des logiques formelles aux applications dans les mondes scientifiques et industriels
Résumé : Longtemps, la logique formelle a été considéré comme seulement un soubassement des mathématiques, pas vraiment utile en pratique. Mais ses progrès ont conduit dans les 30 dernières années à des applications entièrement nouvelles, de grande taille 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 allant de rendre le Sudoku trivial à vérifier systématiquement des propriétés clefs 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 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 coeurs 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.