Projet ANR-15-CE25-0008 – VOCAL : Bibliothèque OCaml vérifiée
Programme : Sciences et technologies logicielles (DS0705) 2015
Année de financement : 2015
Coordinateur du projet : Monsieur Jean-Christophe Filliatre (Université Paris Sud / Laboratoire de Recherche en Informatique)
Partenaires : Inria Centre Paris - Rocquencourt; OCAMLPRO; TPE; Laboratoire public; Laboratoire Verimag
Montant : 645822.0 euros
Date de début : 2015
Durée : 48 mois
Résumé : Le but de ce projet est de développer la première bibliothèque de
structures de données et algorithmes formellement prouvée. Cela peut
paraître surprenant, mais il n'existe à ce jour aucune telle
bibliothèque de grande ampleur, quel que soit le langage de
programmation. Ces dernières décennies ont vu le développement
d'outils de vérification de programmes pour des langages répandus tels
que C ou Java, y compris de notre propre part. Ces efforts ont
conduits à plusieurs succès dans des domaines spécifiques
d'application et sont pertinents pour la vérification de code bas
niveau. Cependant, la vérification, et parfois même la seule
spécification, de code écrit dans ces langages est souvent rendue
complexe par la complexité intrinsèque de leur sémantique, telle que
les nombreuses possibilités d'accès à la mémoire dans le langage C par
exemple. Cette complexité explique sans doute l'absence de
bibliothèques vérifiées dans ces langages.
Dans ce projet, nous faisons le choix d'OCaml, un langage de
programmation qui permet un raisonnement plus facile sur les
programmes, tout en préservant la possibilité d'écrire du code
efficace. Ces deux propriétés expliquent notamment pourquoi OCaml a
été adopté dans le monde entier pour  des applications scientifiques,
industrielles et financières où la stabilité, la sûreté et la
correction sont de la plus haute importance. Des exemples
significatifs sont l'assistant de preuve Coq, les analyseurs statiques
Astrée et Frama-C, le compilateur C optimisant CompCert, le
démonstrateur automatique Alt-Ergo, les logiciels pour la finance de
Jane Street et lexifi ou encore l'outil de transformation de
programmes C Coccinelle. La sémantique claire d'OCaml nous a amené à
développer des outils de vérification pour OCaml ces dernières
années. Ces outils ont maintenant atteint une maturité qui nous laisse
penser que nous pouvons nous attaquer au développement d'une
bibliothèques de structures de données et algorithmes réaliste et
entièrement vérifiée.
Bien que nous faisons le choix d'OCaml, les résultats de notre projet
seront utiles au delà de la communauté OCaml. En effet, les
spécifications et les preuves de notre bibliothèque seront, pour une
large partie, indépendantes du langage de programmation. Ainsi, une
file de priorité réalisée dans le langage C aura essentiellement la
même spécification et les mêmes invariants que sa contrepartie en
OCaml. Nous anticipons ainsi une réutilisation de nos résultats dans
le développement de telles bibliothèques pour d'autres langages et
même pour le développement de bibliothèques multi-langages.
Notre bibliothèques se présentera sous la forme d'un logiciel libre,
directement utilisable par les utilisateurs d'OCaml. En particulier,
elle pourra être utilisée par les développeurs d'outils OCaml
critiques (par exemple Coq, Astrée, Frama-C). En offrant des
composants de programmes vérifiés, nous espérons fournir des briques
de base pour diminuer significativement le coût de développement de
nouveaux programmes vérifiés.
Pour mener à bien notre projet, nous avons réuni une équipe de
chercheurs et de programmeurs qui ont tous une longue expérience du
langage OCaml, de l'assistant de preuve Coq et de la vérification de
programmes. Au delà de notre expérience actuelle en vérification, nous
nous attacherons particulièrement à la modularité et à la
réutilisabilité des spécifications ainsi qu'au support des entiers
machines, ce qui est une condition à l'obtention d'un code efficace
pouvant être intégré dans un logiciel réaliste.