Colloquium d’Informatique de Sorbonne Université
Sandrine Blazy, Université de Rennes
Mardi 26 novembre 2024 18 h
Amphi 25 Sorbonne Université - Faculté des Sciences
Compilation vérifiée : vers du logiciel zéro défaut
Sandrine Blazy est professeure à l'Université de Rennes et directrice adjointe de l'UMR IRISA. Sa thématique de recherche est la vérification formelle de logiciels afin de garantir leur sûreté et leur sécurité. Elle a reçu la médaille d’argent du CNRS en 2023. Avec six collègues, elle a reçu en juin 2022 le prix « ACM software system award » et en juin 2023 le prix « ACM SIGPLAN Programming Languages Software Award » pour le développement du compilateur vérifié CompCert.
Résumé
La vérification déductive permet d’avoir des garanties très fortes sur l’absence de bug dans les logiciels; elle est utilisée pour développer des logiciels embarqués critiques, où toute erreur peut compromettre des vies humaines ou avoir d’autres conséquences catastrophiques. La vérification étant effectuée au niveau source, le compilateur, logiciel complexe et point de passage obligé pour obtenir un code écrit dans un langage compréhensible par la machine mais bien plus primitif, devient un maillon faible dans la chaîne de production du logiciel. Aussi, vérifier le compilateur lui-même permet de garantir qu’aucune erreur n’est introduite lors de la compilation. Plus généralement, cette approche ouvre la voie à la vérification des outils informatiques participant à la production et à la vérification du logiciel. Cet exposé présente les défis sémantiques qu’il a fallu résoudre pour développer CompCert, le premier compilateur optimisant ciblant plusieurs architectures et utilisé dans l'industrie, qui soit doté d’une preuve mathématique de correction vérifiée par ordinateur. Cette preuve se fonde sur un raisonnement sur la sémantique des programmes observés, c’est-à-dire une définition mathématique du comportement de ces derniers. Le code produit par CompCert est garanti se comporter comme prescrit par la sémantique du programme source C. Ce niveau de confiance dans la correction de la compilation permet à CompCert de répondre aux plus hauts niveaux de fiabilité logicielle.
Master Class
L'un des moment particulièrement apprécié lors du colloquium est la « Masterclass » au cours de laquelle quelques doctorants du laboratoires ont l'opportunité de présenter leurs travaux à l'invité(e). Chaque présentation est suivie d'une discussion approfondie. Le programme complet est donné dans le document suivant.
Autres informations
Comité de Pilotage
Informations en ligne
Annonce des Colloquium
Si vous souhaitez être informé des prochains événements, vous pouvez souscrire à la liste de diffusion.
Si vous ne souhaitez plus être informé des événements, vous pouvez vous désinscrire de la liste de diffusion
- Année 2024 – 2025
- Année 2023 – 2024
-
Maurice Herlihy
25 juin 2024
Further Decentralizing Decentralized Finance -
Jean-Marc Jézéquel
04 avril 2024
Comment dompter la variabilité du logiciel ? -
Claire Mathieu
24 janvier 2024
Vehicle routing and approximation algorithms -
David Bol
21 novembre 2023
Six of the nine planetary boundaries are transgressed – How we do research in the Anthropocene?
-
Maurice Herlihy
- Année 2022 – 2023
- Année 2021 – 2022
- Année 2020 – 2021
- Année 2019 – 2020
- Année 2018 – 2019
-
Cláudio T. Silva
11 juin 2019
Urban Data Science -
Sébastiano Vigna
06 mai 2019
Four degrees of separation (and how we did it) -
Hugo Gimbert
19 mars 2019
Les algorithmes de Parcoursup -
Julie Grollier
05 février 2019
Nanodevices for Bio-inspired Computing -
Jacques Pitrat
20 novembre 2018
L'IA forte -
James Larus
23 octobre 2018
Programming Non-Volatile Memory
-
Cláudio T. Silva
- Année 2017 – 2018
-
Eric Horvitz
20 juin 2018
AI Aspirations and Advances -
Justine Cassell
15 mai 2018
Designing Bots, Virtual Humans, and Other Systems that Can Hold up Their End of the Conversation -
Léon Bottou
06 mars 2018
Une approche géométrique de l'apprentissage non supervisé -
Jean-Luc Schwartz
16 janvier 2018
Modélisation cognitive des unités de la parole -
Timothy Roscoe
30 novembre 2017
The Trouble with Hardware
-
Eric Horvitz
- Année 2016 – 2017
-
Simon Peyton Jones
23 mai 2017
Escape from the ivory tower: the Haskell journey -
Maria Chudnovsky
25 avril 2017
Induced subgraphs and coloring -
Philippa Gardner
28 mars 2017
Understanding and Verifying JavaScript Programs -
Michel Beaudoin-Lafon
28 février 2017
Interfaces Homme-Machine -
Marie-Paule Cani
22 novembre 2016
Modélisation 3D expressive -
Richard Stallman
11 octobre 2016
What Makes Digital Inclusion Good Or Bad? -
Patrick Cousot
29 septembre 2016
Abstract interpretation
-
Simon Peyton Jones
- Année 2015 – 2016
-
Patrick Flandrin
16 juin 2016
« Chirps » everywhere -
Aude Billard
12 avril 2016
Robots that exceed human capabilities -
Willy Zwaenepoel
22 mars 2016
Really Big Data -
Jon Crowcroft
19 janvier 2016
Cybersecurity and network measurement -
Isabelle Collet
24 novembre 2015
Les informaticiennes, de la dominance de classe aux discriminations de sexe -
Xavier Leroy
20 octobre 2015
Desperately seeking software perfection
-
Patrick Flandrin
- Année 2014 – 2015
-
Silvio Micali
26 mai 2015
Proofs, Secrets, and Computation -
Alessandra Carbone
14 avril 2015
The new era of biology is computational -
Serge Abiteboul
24 février 2015
Toward personal knowledge bases -
Manuel Silva
25 novembre 2014
Fluidization of discrete event models or a marriage between the discrete and the continuous -
Andrew S. Tanenbaum
28 octobre 2014
MINIX 3: A Reliable and Secure Operating System
-
Silvio Micali
- Année 2013 – 2014
-
Donald Knuth
17 juin 2014
Computer Science: All Questions Answered -
Jeannette Wing
20 mai 2014
Toward a Theory of Trust in Networks of Humans and Computers -
David Patterson
06 mai 2014
Myths about MOOCs and Software Engineering Education -
Claude Berrou
25 mars 2014
L'information mentale -
Vint Cerf
04 mars 2014
On the Preservation of Digital Information -
C.A.R. (Tony) Hoare
26 novembre 2013
Laws of concurrent system design -
Gilles Dowek
22 octobre 2013
Are formal methods the future of air traffic control?
(Is there an autopilot on board?)
-
Donald Knuth
- Année 2012 – 2013
-
Mathieu Feuillet, Camille Couprie, Mathilde Noual
25 juin 2013
Espoirs : Winners of the 2012 Gilles Kahn prize -
Robert Sedgwick
23 mai 2013
Taking Education Online: A Unique Opportunity for the New Millenium -
Frans Kaashoek
18 avril 2013
The multicore evolution and operating systems -
Stuart Russell
22 janvier 2013
Unifying logic and probability: A “New Dawn” for Artificial Intelligence? -
Georges Gonthier
27 novembre 2012
Le génie mathématique, du théorème des quatre couleurs à la classification des groupes -
Gérard Berry
24 octobre 2012
Le temps et les événements en informatique
-
Mathieu Feuillet, Camille Couprie, Mathilde Noual
- Année 2011 – 2012