Verifying Code That Calls Code You Can't Trust • Sophia Drossopoulou • Bug Bash EU 2026

Valeur des informations & solidité de l’argumentation

L’apport principal réside dans la combinaison de protection et d’invariants scopés pour raisonner sur des appels externes non fiables, avec une formalisation précise et une discussion des limites comme les spécifications circulaires. L’argumentation s’appuie sur des exemples concrets (boutique, escrow) et des preuves de solidité de l’inférence, bien que certaines étapes soient seulement esquissées. La valeur est indéniable pour la recherche en vérification de programmes.

Rigueur scientifique, qualité des sources, adéquation du titre

La rigueur scientifique est élevée : l’intervenante cite des collaborateurs (Mark Miller, James Noble) et des travaux antérieurs, mais sans donner de références bibliographiques précises dans l’exposé. Le titre est fidèle au contenu, qui porte effectivement sur la vérification de code interagissant avec du code non fiable. La présentation est un travail de recherche original, susceptible d’intéresser les spécialistes.

Le titre correspond exactement au contenu : il s'agit de la vérification de code interagissant avec du code non fiable, avec des exemples concrets et des solutions formelles.

9/10

Exposé par une chercheuse reconnue, s'appuyant sur des preuves formelles et une démarche originale. La présentation est cohérente et bien structurée, bien que les preuves ne soient pas pleinement approfondies à l'écran.

Repères établis par PSI à partir de la transcription : le créateur n'a pas défini de chapitres.

• 00:00Introduction et contexte : collaboration de 10 ans sur l'encapsulation et les garanties dans les systèmes ouverts.
• 04:00Exemple motivant : boutique, compte et clé, et le problème des effets des appels externes.
• 08:00Définition de la protection et des invariants scopés comme fondements de la spécification.
• 14:00Système d'inférence : passage de triples de Hoare à des quadruplets pour raisonner sur les états intermédiaires.
• 20:00Outil de vérification : prototype de traduction vers Dafny pour automatiser les preuves.
• 26:00Médiation et exemple d'escrow : spécification du risque et de la confiance entre parties.
• 32:00Spécifications circulaires et solution par stratification pour éviter le paradoxe de Russell.
• 37:00Résumé des six remits, état d'avancement et perspectives de mécanisation.

• Bug Bash EU 2026 — Page officielle de la conférence où la présentation a été enregistrée.
• Bluesky de GOTO Conferences — Compte Bluesky de la chaîne organisatrice.
• LinkedIn de GOTO Conferences — Page LinkedIn de la société GOTO.
• LinkedIn de Sophia Drossopoulou — Page LinkedIn de l'intervenante.