Défis de génie logiciel dans l'évolution collaborative de l'assistant de preuve Coq et son écosystème
Exposé invité de Théo Zimmermann (Inria, Université de Paris, IRIF, CNRS) le 27 février 2020 à 16h-17h.
Coq est un assistant de preuve servant à la fois à la validation de preuves mathématiques et à la vérification de propriétés de programmes. Il est développé principalement par des chercheurs Inria depuis plus de 35 ans. Logiciel libre, son développement est aujourd’hui entièrement ouvert et transparent, et organisé autour de la plateforme GitHub. Les développeurs de Coq font face à de nombreuses questions standards de génie logiciel que la complexité de ce logiciel ne fait que renforcer : dette technique, tests, sortie de nouvelles versions, compatibilité, documentation, accueil de nouveaux contributeurs, etc. Le développement de processus et d’outils DevOps permet d’y remédier. Un défi supplémentaire est celui d’organiser la communauté pour améliorer la qualité, pas seulement de Coq lui-même, mais aussi de son écosystème (bibliothèques, plugins, outils, tutoriels…).
- Intervenant : Théo Zimmermann
- Affiliation : Inria, Université de Paris, IRIF, CNRS
- Date : 2020-02-27
- Heure : 16h-17h
- Lieu : Université Paul Sabatier - IRIT - Auditorium Herbrand
Cet exposé s’inscrit dans le cadre des conférences organisées par le parcours DL du Master Informatique.
Pour faciliter l’organisation, merci aux extérieurs de s’inscrire dès que possible en remplissant ce formulaire.
Pour continuer la discussion avec l’orateur, l’exposé sera suivi d’un goûter à la caféteria de l’IRIT.