14:00
15:00

Le développement logiciel est un processus intrinsèquement incrémental. À cette fin, la plupart des langages de programmation fournissent aux programmeurs des mécanismes de base leur permettant d’indiquer qu’une fonctionnalité donnée n’est pas encore implémentée, par exemple au moyen d’exceptions dédiées. Malheureusement, à l’exception des vérificateurs de types incrémentaux, la plupart des outils utilisés pour raisonner sur la correction des programmes — tels que les cadres de test, d’analyse et de vérification — ne tiennent pas compte de ces idiomes d’incomplétude. En conséquence, les programmeurs sont confrontés soit à des rapports d'échec erronés, soit à la charge de modifier leurs spécifications, ce qui sacrifie le lien de causalité direct entre le code et les outils de raisonnement. Dans cette présentation, j'illustrerai ce problème dans le contexte des tests, en considérant à la fois les tests unitaires et les tests basés sur les propriétés, ainsi que la programmation certifiée dans les assistants de preuve. L'examen du problème dans des contextes aussi disparates nous permet d'isoler les concepts fondamentaux nécessaires à la construction d'outils de raisonnement véritablement incrémentaux.

Biographie :
Éric Tanter est professeur titulaire au département d'informatique de l'Université du Chili. Il a obtenu son doctorat conjointement à l'Université de Nantes et à l'Université du Chili en 2004. Ses recherches portent sur les langages de programmation et le génie logiciel, allant des fondements théoriques des langages de programmation à l'étude empirique des pratiques de programmation. Récemment, il s'est fortement impliqué dans les fondements et la pratique du typage et de la vérification graduels. Il occupe une chaire internationale de l'Inria pour la période 2025-2029.
 

Salle 178 (LaBRI)