Room 206 (2nd floor, badged access)
7 mars 2024 - 14h30
Développement logiciel formellement vérifié: pourquoi et comment ?
par Sylvain Boulmé de Verimag, Grenoble-INP Ensimag
Résumé : Dans le cadre de ma candidature au poste de professeur Polytech/Verimag, je tracerai un panorama de mes travaux sur le développement logiciel formellement vérifié, depuis que j'ai commencé (il y a presque 30 ans). Je situerai ces travaux dans les problématiques du génie logiciel: comment limiter l'impact des bugs dans les logiciels; comment rendre ces développements modulaires et réutilisables; comment alléger la pénibilité des preuves formelles (e.g. en exploitant les changements de représentation et le typage); en quoi la programmation défensive permet de cumuler tous ces objectifs... Le tout sera illustré sur des applications allant d'un système de calcul formel à la compilation bas-niveau.
