JFLA 2015 : articles de recherche

Abstract: E-ACSL est un greffon de Frama-C, une plateforme d'analyse de codes C qui est développée en OCaml. Son but est de transformer un programme C formellement annoté dans le langage de spécification éponyme E-ACSL en un autre programme C dont le comportement à l'exécution est équivalent si toutes les spécifications sont dynamiquement vérifiées et qui échoue sur la première spécification fausse sinon.

Cet article présente deux analyses statiques qui améliorent grandement la précision de cette transformation de programme en réduisant l'instrumentation effectuée. Ainsi, le code généré est plus rapide et consomme moins de mémoire lors de son exécution. La première analyse est un système de types permettant de distinguer les entiers (mathématiques) pouvant être convertis en des expressions C de type <<entier machine>> de ceux devant être traduits vers des entiers en précision arbitraire. La seconde analyse est une analyse flot de données arrière paramétrée par une analyse d'alias. Elle permet de limiter l'instrumentation des opérations sur la mémoire à celles ayant un impact potentiel sur la validité d'une annotation formelle.

Abstract: Using Coq, we mechanize Wegener's proof of Kosaraju's linear-time algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depth-first search algorithm.

Abstract: We present a static control flow analysis used in the Simple Unified Policy Programming Language (Suppl) compiler to detect internally inconsistent policies. For example, an access control policy can decide to both ``allow'' and ``deny'' access for a user; such an inconsistency is called a conflict. Policies in Suppl follow the Event-Condition-Action paradigm; predicates are used to model conditions and event handlers are written in an imperative way. The analysis is twofold; it first computes a superset of all conflicts by looking for a combination of actions in the event handlers that might violate a user-supplied definition of conflicts. SMT solvers are then used to try to rule out the combinations that cannot possibly be executed. The analysis is formally proven sound in Coq in the sense that no actual conflict will be ruled out by the SMT solvers. Finally, we explain how we try to show the user what causes the conflicts, to make them easier to solve.

Abstract: Dans cet article, on se propose d'utiliser les développements récents de sémantique des jeux basés sur des ordres partiels pour donner une sémantique dénotationnelle à une primitive de concurrence inspirée de l'appel système UNIX fork. Cet appel système, lors de son invocation, duplique le contexte d'exécution de son programme, et renvoie deux entiers distincts permettant au programme de savoir dans quelle dent de la fourche il se trouve.

La première contribution de cet article est de donner une sémantique opérationnelle faisant droit au parfum opérateur de contrôle de cette primitive qui manipule le contexte d'exécution. La seconde contribution de ce papier est l'élaboration d'une sémantique des jeux « vraiment concurrente » qui donne une représentation fine de l'exécution du langage.

Cette sémantique des jeux est prouvée correcte vis-à-vis de la sémantique opérationnelle et permet de faire un premier pas vers la modélisation de comportements concurrents complexes en utilisant les jeux concurrents.

Abstract: We are interested in the problem of expressiveness of the following operations in the category of sets: finite products and coproducts, initial algebras (induction) and final coalgebras (coinduction). These operations are the building blocks of a logical system that allows circularity in Gentzen-style proofs. Proofs in this system are seen as simple programs, while the cut-elimination process is viewed as a running automaton with a memory device. In this paper, we show that higher-order trees, those accepted by higher-order pushdown automata, are computable in this setting, by providing an explicit simulation of the automata by cut-elimination.

Abstract: Le (bon) séquencement des événements au fil du temps fait partie des nombreux sujets d'analyse de programmes, par exemple pour l'étude de protocoles d'échange d'information ou de systèmes embarqués. De nombreux travaux de logique temporelle linéaire (LTL) permettent de décrire formellement le comportement attendu d'un programme, sous la forme d'une succession d’actions distinctes.

Implanté au sein de Frama-C, plate-forme d'analyse de code source en langage C, le greffon Aoraï permet la génération de spécifications équivalentes, dans leur ensemble, à la conformité d'un programme C donné vis à vis d'une formule de logique temporelle linéaire. Ce greffon discrétise le temps de telle sorte que seuls les appels et les retours de fonctions sont considérés comme des événements. Cet article présente Model-CaRet, un nouveau greffon Frama-C qui généralise la trace étudiée par Aoraï. Plus précisément, Model-CaRet est dédié à la génération du test de satisfiabilité, et à sa vérification automatique, d'une formule de logique CaRet sur un programme C, représenté sous la forme d'une machine à états récursif. CaRet est une extension naturelle de la LTL permettant l'étude simultanée de plusieurs traces d'exécution, et en particulier de manipuler explicitement la pile d'appel du programme dans les formules.

Abstract: Nous présentons une expérience qui vise à certifier un compilateur de manière la plus automatique possible. À cette fin, nous avons choisi un exemple jouet, présenté par Xavier Leroy lors d'un cours à l'OPLSS sur la vérification mécanisée des compilateurs, qui effectue la traduction d'un langage impératif simple vers une machine virtuelle. Bien que relativement modeste, ce choix suffit à illustrer la complexité des problèmes rencontrés. Un autre intérêt est que ce compilateur est accompagné d'une preuve Coq qui nous fournit un élément de comparaison.

Nous avons mené cette expérience en utilisant l'environnement de preuve de programme Why3, ce qui nous permet de décharger les obligations de preuves à l'aide de prouveurs, notamment automatiques. Nous avons d'abord tenté une approche directe, dans l'esprit de la preuve Coq. Cependant, elle s'est montrée peu satisfaisante : les prouveurs automatiques s'avèrent incapables de trouver les états intermédiaires de l'exécution, ce qui nous oblige à les exhiber manuellement.

Si l'on voit la preuve d'un compilateur comme la vérification que le code généré satisfait une spécification (dérivée du code source), on peut ramener la correction du compilateur à la correction du code qu'il produit. L'approche que nous présentons dans cet article consiste à exploiter des méthodes de preuve de programmes, proches de celles employées par Why3 lui-même, au niveau du code généré. Une telle méthode rend la preuve du compilateur quasi-automatique.

Abstract: We consider a recent publication on higher-order process calculi and describe how its results are formalized in the Coq proof assistant. We also highlight some important technical issues that we have uncovered in the original publication. We believe these issues are not unique to the paper under consideration, and require particular care to be avoided. Our ultimate goal is to show that it is possible to build a solid, high-confidence setting for formal reasoning on higher-order process calculi.

Abstract: De nombreux outils sont aujourd'hui disponibles pour l'analyse et la production temps réel de flux média temporisés: sons, video, animations, etc... Néanmoins, la coordination de ces outils, la synchronisation des flux qu'ils analysent et produisent, sur des échelles de temps de valeurs et même de nature différente, reste une affaire délicate.

Le modèle des Tiled Polymorphic Temporal Media (ou TPTM), qui combine en un même formalisme le contenu media de ces flux et leurs marqueurs de synchronisations, vise a remédier à cela. Dans le modèle, le produit de deux flux ainsi enrichis, paramétré par ces marqueurs de synchronisations, est tout à la fois séquentiel et parallèle: c'est un produit tuilé.

En théorie, la sémantique des ces flux tuilés peut être décrite dans la théorie des monoïdes inversifs. En pratique, nous proposons ici, en Haskell, la première implémentation réellement polymorphe et inversive de ces TPTM. Notre implémentation permet en outre, via le mécanisme d'évaluation paresseuse d'Haskell, de distinguer simplement la syntaxe de ces flux (un système d'équations tuilés) de leurs sémantiques opérationnelles (la résolution de ce système à la volée).

Abstract: Le théorème de Thalès pour les cercles et sa réciproque (plus connue sous le nom de théorème du cercle circonscrit à un triangle rectangle) sont des propriétés de géométrie élémentaire enseignées dans les collèges français. Nous nous intéressons non seulement à différentes descriptions possibles de ces propriétés en Coq mais aussi aux preuves correspondantes. Nous étudions notamment comment le choix d’une représentation des objets géométriques contenus dans l’énoncé influencent les arguments de preuve. Nous présentons plusieurs approches, une basée sur des calculs d’angles, une autre basée sur la géométrie analytique et finalement deux démonstrations différentes dans l’axiomatique de Tarski en utilisant dans un cas le théorème de la droite des milieux et dans l’autre la notion de symétrie centrale et ses propriétés.

Abstract: La récupération automatique de la mémoire est une caractéristique commune des langages de programmation. Elle offre certes au programmeur des garanties de fiabilité, mais, en éloignant ce dernier des détails de la gestion de la mémoire, elle rend plus difficile la compréhension et, a fortiori, la maîtrise des allocations de mémoire.

Dans ce papier, nous présentons les résultats de nos travaux sur l'analyse du comportement mémoire des programmes OCaml. Nous présentons une technique basée sur la modification des en-têtes des blocs permettant de récupérer une information de type partielle sur chaque bloc tout en préservant le même comportement mémoire que le programme original. Ces informations de type sont enrichies ultérieurement par une technique de reconstruction de type par unification. Des algorithmes de graphes peuvent ensuite être appliqués dans le but d'obtenir des informations plus fines.

Nous présentons également quelques cas d'usage montrant comment l'utilisation de ces techniques a permis d'optimiser plusieurs logiciels tel que Alt-Ergo et Ocsigen.

Abstract: Nous vérifions automatiquement des programmes impératifs d'énumération de structures combinatoires implantées dans des tableaux satisfaisant certaines propriétés structurelles. Ces programmes C sont spécifiés en ACSL et vérifiés avec la plateforme Frama-C. La vérification déductive démontre automatiquement que tous les tableaux produits ont les propriétés attendues. Elle est facilitée par sa combinaison avec des analyses dynamiques, qui permettent aussi de valider d'autres propriétés des programmes, comme leur complétude. Nous proposons une bibliothèque de programmes vérifiés et des patrons de programmation et de spécification facilitant leur conception et leur mise au point. Ces programmes trouvent une application naturelle dans le test exhaustif borné de programmes manipulant ces tableaux.

Abstract: Irmin is an OCaml library to persist, merge and synchronize purely functional datastructures. In this paper, we focus on the merge aspect of the library and present two datastructures built on top of Irmin: (i) mergeable queues and (ii) mergeable ropes, which extend the corresponding purely functional datastructures with a 3-way merge operation. We provide theoretical and practical complexity results for these new datastructures. Irmin is available as open-source code as part of the Mirage OS project.

Abstract: Families of binary relations are important interpretations of regular expressions, and the equivalence of two regular expressions with respect to their relational interpretations is decidable: the problem reduces to the equality of the denoted regular languages.

Putting together a few results from the literature, we first make explicit a generalisation of this reduction, for regular expressions extended with converse and intersection: instead of considering sets of words (i.e., formal languages), one has to consider sets of directed and labelled graphs.

We then focus on identity-free regular expressions with converse—a setting where the above graphs are acyclic—and we show that the corresponding equational theory is decidable. We achieve this by defining an automaton model, based on Petri Nets, to recognise these sets of acyclic graphs, and by providing an algorithm to compare such automata.

Abstract: For those of us that generally live in the world of syntax, semantic proof methods such as realizability or logical relations / parametricity sometimes feel like magic. Why do they work? At which point in the proof is "the real work" done?

Bernardy and Lasson express realizability and parametricity models as syntactic model -- but the abstraction/adequacy theorems are still explained as meta-level proofs. Hoping to better understand the proof technique, we look at those theorems as programs themselves. How does a normalization proof using realizability actually computes those normal forms?

This detective work is an early stage and we propose a first attempt in a simple setting. Instead of arbitrary Pure Type Systems, we use the minimal negative propositional logic (arrows only). Instead of starting from the simply-typed lambda-calculus, we work on sequent-style terms in a simple subset of the Curien-Herbelin L calculus.

Abstract: Nous proposons une formalisation en Coq des graphes orientés et non orientés et des notions associées. La bibliothèque développée offre non seulement l'expressivité requise pour exprimer et démontrer des propriétés sur les graphes mais aussi une implantation purement fonctionnelle permettant de mettre en oeuvre efficacement les algorithmes de graphe. Nous spécifions ensuite à l'aide de cette bibliothèque les notions de couplage et d'ensemble de sommets couvrant et développons un vérificateur formellement vérifié dont l'objectif est de certifier le résultat d'un fonction qui calcule un couplage maximal. Le code exécutable de ce vérificateur est obtenu grâce au mécanisme d'extraction de Coq. Ce travail est une première contribution d'un projet plus ambitieux qui concerne le développement d'un algorithme de filtrage formellement vérifié pour la contrainte de différence (alldiff) pour des domaines finis. Ce dernier algorithme utilise de nombreuses manipulations de graphe dont le calcul d'un couplage maximal.

Abstract: We present a linearization method to over-approximate non-linear multivariate polynomials with convex polyhedra. It is based on Handelman's theorem and consists in using products of constraints of a starting polyhedron to over-approximate a polynomial. We implemented it together with two other linearization methods that we will not detail in this paper, but that we shall use as comparison.