Je m'intéresse à la sûreté de programmation, notamment à la qualité de l'arithmétique, ainsi qu'aux preuves formelles mécanisées.
Un petit lien vers FOC pour voirÀ partir de la couche assembleur, de la version C et de la description de la version Lisp du package d'arithmétique rationnelle exacte BigNum développé à l'Inria, j'ai écrit pendant ma thèse la version Caml de BigNum
- Efficace, flexible, puissant, aisé à utiliser, intégrée au langage
- Conçue et implémentée en Caml V3.1
- Adaptée pour Caml Light par Xavier Leroy, pour Caml Special Light, le prédécesseur d'Objective Caml, par Victor Manuel Gulias Fernandez
- Maintenue par Pierre Weis
- La couche de bas niveau sans allocation n'est plus fournie par BigNum pour s'affranchir de ses problèmes de licence, elle a été entièrement réécrite par Xavier Leroy et utilise les inline extended asm de gcc
Vingt ans d'arithmétique réelle: le comblement progressif d'un fossé entre le résultat faux tout de suite et le résultat correct trop tard
L'arithmétique réelle en précision arbitraire
Les enjeux d'une arithmétique réelle en précision arbitraire- L'état de l'arithmétique des ordinateurs aujourd'hui:
- Les processeurs forunissent des entiers bornés et des nombres flottants.
- C'est nettement insuffisant à l'heure actuelle où les besoins de précision de nombre de calculs grandissent et où la vitesse des ordinateurs permet d'envisager d'aller plus loin (par exemple nombre d'applications graphiques névessitent de calculer avec des flottants de plusieurs mots voire davantage).
- Par ailleurs certains algorithmes théoriques ne sont corrects que si certaines propriétés sont vérifiées et il faut donc pouvoir assurer par une précision convenable ces propriétés au cours d'une chaîne algorithmique (par exemple ce besoin est particulièrement sensible en calcul scientifique).
- Un programme décrit dans un bon langage peut fournir un résultat avec toute la précision requise par le programmeur, mais une erreur dans l'algorithme ou dans le programme qui l'implémente retire tout intérêt à cette précision. Il est donc aussi important dans une chaîne du logiciel sûre de pouvoir prouver les programmes que l'on écrit.
Mes publications sur l'arithmétique exacte
- The CAML Numbers Reference Manual: rapport technique de 160 pages ( Résumé, Référence BibTeX)
- Une arithmétique rationnelle exacte efficace en CAML: article de conférence court ( Résumé, Référence BibTeX)
- (avec Pierre Weis) An exact arithmetic package for ML: article court à paraître dans SCP ( Résumé, Référence BibTeX)
- Arithmétique exacte: conception, algorithmique et performances d'une implémentation informatique en précision arbitraire: version finale de ma thèse 202 pages ( Résumé, Référence BibTeX)
- Conception et algorithmique d'une représentation arithmétique réelle en précision arbitraire: article de conférence court (Résumé, Référence BibTeX)
- Arbitrary precision real arithmetic: design and algorithms: article long soumis à JSC ( Résumé, Référence BibTex)
La preuve formelle mécanisée
- Contribution au développement de preuves dans le système d'aide à la démonstration Coq
- arithmétique
- algorithme de typage de ML (travail avec Catherine Dubois)
- protocoles cryptographiques (travail au sein du GIE Dyade avec Dominique Bolignano notamment)
Mes publications sur la preuve formelle mécanisée
- (avec Catherine Dubois)) A proved type inference tool for ML: Damas-Milner within Coq (work in progress: article de conférence court ( Résumé, Référence BibTeX)
- (avec Catherine Dubois)) Certification of a type inference tool for ML: Damas-Milner in Coq: article soumis au numéro spécial «Formal Proof» de JAR( Résumé, Référence BibTeX)
- (avec Dominique Bolignano ) Formal verification of cryptographic protocols using Coq: article soumis au numéro spécial «Formal Proof» de JAR( Résumé, Référence BibTeX)
- Coq tacticals considered powerful: thoughts about methodology of proof: rapport de recherche à paraitre ( Résumé, Référence BibTeX)
Quelques preuves formelles en Coq
- preuve de correction de l'algorithme de typage de ML, répertoire des fichiers sources tar-gzippé
- preuve de correction du protocole cryptographique Otway-Rees, répertoire des fichiers sources tar-gzippé
- preuve de correction de l'algorithme de typage de ML, fichiers sources hypertextes
