JFLA 2020

Nous étudions la vérification formelle de programmes avec effets de bord en utilisant un langage purement fonctionnel. Dans le cadre de cette étude, nous avons développé Monae, une librairie Coq qui propose une formalisation des monades et de leurs lois algébriques. Les preuves se font par raisonnement équationnel en utilisant les capacités de réécriture de Coq. Les programmes n’utilisent généralement pas un seul type d’effet de bord, mais une combinaison de plusieurs d’entre eux. On utilise les transformateurs de monades dans ce but. Cependant, l’approche traditionnelle pour le lifting des primitives n’est pas modulaire. Il est intéressant de définir de manière canonique les opérations algébriques des monades et leurs primitives lift. Dans cet article, nous présentons l’implémentation des transformateurs de monades modulaires et les preuves des théorèmes qui en découlent en Coq. Nous montrons également leurs utilisations comparées aux transformateurs de monades classique.

Les langages synchrones ont été introduits pour la conception de systèmes embarqués temps-réel. Ces langages dédiés permettent de décrire précisément les spécifications du système, et ainsi de le simuler, le tester, le vérifier, et finalement le compiler en du code exécutable. Cependant, ces langages offrent un support limité pour modéliser les comportements non-déterministes qui sont omniprésents dans les systèmes embarqués. ProbZélus est une récente extension probabiliste d’un langage synchrone descendant de Lustre. ProbZélus permet de décrire des modèles probabilistes réactifs, c’est-à-dire, en interaction avec un environnement observable. Lors de l’exécution, un ensemble de techniques d’inférence peut être utilisé pour apprendre les distributions de paramètres latents du modèle à partir de données observées. Dans cet article nous illustrons l’expressivité de ProbZélus avec des exemples comme un détecteur de trajectoire à partir d’observations bruitées, ou un contrôleur de robot capable d’inférer à la fois sa position et une carte de son environnement.

Jusqu’à la version 8.10 de Coq, les nombres réels de la bibliothèque standard étaient axiomatisés, de façon semi-classique. Ceci posait 3 problèmes : la cohérence de ces axiomes n’était pas formellement prouvée (elle était informellement dérivable du modèle ensembliste de Coq étendu avec l’axiome du choix et la logique classique), ces axiomes bloquaient les calculs (la réduction sous forme normale des approximations rationnelles) et enfin l’utilisateur ne pouvait pas se restreindre aux nombres réels constructifs.

Nous présentons une découpe des nombres réels de Coq en une première couche constructive et sans axiome, suivie d’une seconde couche qui donne les nombres réels classiques par quotient de la première couche. L’absence d’axiome dans la couche constructive établit sa cohérence avec le coeur de Coq, c’est-à-dire le calcul des constructions inductives. Elle garantit également la terminaison des calculs, ce qui est conforme aux attentes des mathématiques constructives. La seconde couche classique introduit quelques axiomes, qui sont vrais dans le modèle ensembliste de Coq, leur cohérence est donc prouvée. Enfin l’utilisateur a désormais le choix d’utiliser les nombres réels constructifs ou classiques, selon quels fichiers de la bibliothèque standard il importe.

Cette découpe a été intégrée dans la bibliothèque standard de Coq le 5 août 2019, pour une sortie dans la prochaine version 8.11. Elle est rétro-compatible: toutes les bibliothèques (Coquelicot, Flocq, VST, …) qui utilisaient les nombres réels de Coq jusqu’à la version 8.10 continuent de compiler et de fonctionner, sans aucune modification de leur code source.

TLA+ is a specification language based on traditional untyped set theory. It is equipped with a set of tools, including the TLA+ proof system TLAPS, which uses trusted back-end solvers to handle individual proof steps – referred to as “proof obligations”. As most solvers rely on and benefit from typed formalisms, types are first reconstructed for the obligations; however, the current encoding into the SMTlib format does not exploit all of this type information. In this paper, we present motivations for a more pervasive usage of types at an intermediate representation of TLA + proof obligations, and describe work in progress on several improvements of TLAPS: a type-driven SMT encoding, a tactic for instantiation hints, and type annotations for the language. We conclude with some perspectives for future work.

Learn-OCaml est un logiciel libre destiné à l’enseignement du langage OCaml : il fournit un environnement d’exercices de programmation à correction automatisée. On propose une extension du code source de Learn-OCaml, permettant la séparation et la réutilisation du code de correction et simplifiant l’écriture de tests. Cette extension donne lieu, dans un second temps, à l’élaboration d’une bibliothèque d’aide à la conception d’exercices en Learn-OCaml qui permet de construire des rapports de correction plus adaptés aux constructions avancées du langage. Ces outils ont permis de porter plusieurs séries d’exercices en OCaml utilisées dans des cours de programmation à Sorbonne Université permettant ainsi un premier retour d’expérience positif.

Dans cet article, nous nous intéressons au problème du calcul de la hauteur d’un arbre. Le problème a l’air plutôt simple, à priori, puisqu’il suffit de suivre la définition mathématique avec unesimple fonction récursive de quelques lignes. Néanmoins, une tellefonction peut facilement faire déborder la pile d’appels. Après avoir laissé le lecteur réfléchir à une solution, nous en discutons plusieurs, notamment au regard de ce qu’offre le langage de programmation. Ce problème illustre la difficulté qu’il peut y avoir à se passer de récursivité.

Le développement en C de logiciels non-critiques utilise régulièrement l’insertion d’assembleur « en ligne », que ce soit pour optimiser certaines opérations ou pour accéder à des primitives systèmes autrement inaccessibles. Celui-ci demande l’écriture de spécifications sous forme de contraintes pour faire le lien entre le langage hôte (C) et le langage assembleur embarqué. Ces spécifications sont ensuite utilisées par le compilateur pour pouvoir insérer l’assembleur dans le code émis, en croyant le programmeur sur parole. Pour éviter les erreurs issues de spécifications mal formées, nous proposons RUSTInA, un outil qui permet de vérifier que les spécifications assembleurs correspondent bien à l’implémentation des blocs qu’elles décrivent, ou, dans le cas contraire diagnostiquer ou corriger le problème.

Chez OCamlPro, notre usage de OCaml a changé. Là où nous faisions majoritairement des programes terminant, notre modèle d’affaire s’est élargi nous menant à concevoir des systèmes sensés fonctionner pendant de longues durées. Pour ces usages, la manière typique de débogguage de OCaml à grand coup de Printf n’est pas adaptée. En particulier pour les fuites mémoires lentes, difficilement observables hors de la production. Imaginons, au hasard, un serveur maintenant une chaîne-de-blocs qui fuiterait quelques octets par connections. En fonctionnement normal, cela est perdu dans le bruit du glaneur de cellules (GC). Mais un attaquant le découvrant pourrait facilement en profiter pour disrupter le service. Nous proposons une solution intégrée, pour découvrir, analyser et traiter cette problématique sur des logiciels déployés. Un outil d’analyse statistique léger permettant de collecter à un coût modeste et en continu les schémas d’allocations et de désalloctions. Celui ci est couplé à un mechanisme de collecte exaustive du graphe mémoire utilisé quand un problème est identifié. Y est adjoint une interface utilisateur pour cibler l’attention du dévelopeur vers les points clefs et le guider vers la correction.

The past decade has seen renewed interest in the formal, mechanized verification of compilers, as evidenced by the success of both, CakeML and CompCert. In addition, muttiple smaller compilers or compilation phases get mechanically formalized at an increasing pace. More often than not, these small-scale formalizations lack common abstractions and definitions: they have slightly different ways of encoding the languages’ semantics, compilation functions, how they compose, etc. Time and again, general correctness lemmas — such as forward and backward simulation — need to be defined and proven again and again. Simply put, the idea of reuse has not been adopted on a broader scale. In this article, we present a prototype version of a generic framework for formalizing compiler transformations. Specifically, our framework leverages Isabelle/HOL’s locales to abstract over concrete languages and transformations. The framework thus enables us to state common definitions for language semantics, program behaviours, forward and backward simulations, and compilers. We provide generic operations, such as compiler composition, and prove general theorems, resulting in reusable proof components. By demonstrating our idea on a concrete example, we provide evidence of how locales allow reuse and, therefore, enable encapsulation of verification artifacts into modules.