Vérification Interactive de Programmes Fonctionnels

Arthur Chargéraud (Inria Rocquencourt)

La description de la syntaxe et de la sémantique d'un langage de programmation dans un assistant de preuve permet de raisonner sur des programmes écrits dans ce langage. Dans cet exposé, j'expliquerai comment suivre cette approche pour spécifier et vérifier en Coq des programmes écrits dans le fragment purement fonctionnel de Caml.

Preuve modulaire de programmes impératifs d'ordre supérieur

Johannes Kanig (INRIA Saclay)

Nous proposons une logique de Hoare pour un langage de programmation impératif avec des fonctions d'ordre supérieur. Nous nous plaçons dans le cadre simple du lambda-calcul avec des références globales, sans alias. Une combinaison de typage à effets polymorphes avec une logique d'ordre supérieur permet de raisonner modulairement sur des programmes d'ordre supérieur. Nous argumentons qu'il est possible d'adapter ce système à un langage, toujours sans alias, dans lequel les références sont de première classe.

Dépasser les limites de la co-récursion gardée par les constructeurs

Yves Bertot (INRIA Sophia Antipolis)

Les structures de données infinies sont disponibles dans les langages de programmation Ocaml ou Haskell et dans les systèmes de démonstration comme Coq. Les pouvoirs expressifs ne sont pas comparables: le typage simple restreint les langages de programmation, l'obligation de décrire des programmes qui terminent ou qui sont productifs restreint les systèmes de preuve.
En particulier, Coq autorise les structures de données infinies par le biais des types co-inductifs en imposant une forme de récursion restreinte "gardée par les constructeurs" qui interdit le codage direct de nombreuses valeurs qui sont faciles à définir dans les langages de programmation. Dans cet exposé, nous décrivons des techniques, partant de la définition acceptable en Haskell, pour obtenir une valeur acceptée en Coq qui respecte la définition, ce qui permet ensuite de faire des preuves sur la valeur de ces programmes.
Une partie de ce travail a été réalisé en collaboration avec Ekaterina Komendantskaya.

Analyse de flôt d'information pour les systèmes embarqués

Dorina Ghindici (LIFL)

Ces travaux ont pour but de fournir une solution aux problèmes de confidentialité dans les systèmes multi-applicatifs: assurer la sécurité des applications dédiées aux systèmes portables et autonomes en vérifiant des propriétés de sécurité en termes de flot d'information au moment du chargement des applications, contrairement aux travaux existants qui ne sont ni modulaires ni dynamiques. Nous proposons un modèle et un outil adaptés aux contraintes inhérentes aux systèmes embarqués. Notre approche est modulaire et supporte l'héritage et la surcharge. La vérification est donc incrémentale et s'effectue sur le système cible, le seul endroit ou la sécurité peut être garantie. Il s'agit, à notre connaissance, du premier vérifieur embarqué pour l'analyse de flot d'information. Afin de prouver l'utilité pratique de notre modèle, nous avons mené des expérimentations et nous avons testé l'outil dans des contextes différents.

Conception, spécification et preuve formelle d'un algorithme de calcul d'enveloppe convexe avec des hypercartes en Coq

Christophe Brun (LSIIT Strasbourg)

Notre objectif de mener une étude formelle dans le domaine de la modélisation et de la géométrie algorithmique, afin d'améliorer les techniques de programmation et d'assurer la correction des algorithmes. Nous faisons une étude de cas en géométrie algorithmique en nous intéressant à un problème classique qui met en jeu la subdivision de surface la plus simple : le calcul incrémental de l'enveloppe convexe d'un ensemble fini de points du plan. L'originalité des moyens utilisés s'appuie d'une part sur les spécifications et les preuves formelles de programmes qui sont exprimées dans le formalisme du calcul des constructions inductives mis en oeuvre dans le système d'aide à la preuve Coq, et de l'autre sur le fait que nous utilisons un cadre de modélisation géométrique à base topologique où les subdivisions de surface sont représentées par des hypercartes. Une hypercarte est une structure algébrique fondée sur les notions de brins et de permutations, qui permet de modéliser les subdivisions du plan en séparant bien les aspects topologiques et géométriques des objets étudiés. Elle se décrit aisément par induction structurelle. Notre travail consiste en la conception d'un algorithme fonctionnel, l'extraction automatique d'un programme en Ocaml permettant la saisie des données et une visualisation graphique du résultat, et la preuve formelle de sa correction totale par la vérification de sa terminaison et la mise en évidence de nombreuses propriétés topologiques et géométriques.

Réécriture topologique, vers une géométrisation de la programmation

Antoine Spicher (Creteil, LACL)

Spatial computing is an emerging field that recognizes the importance of explicitly handling spatial relationships at three levels: computer architectures, programming languages and applications. In this context, we present MGS, an experimental programming language where data structures are fields on abstract spaces. In MGS, fields are transformed using rules. The MGS notions of topological collection and transformation are formalized using concepts developed in algebraic topology. We propose to use transformations in order to implement a discrete version of some differential operators. These transformations satisfy a Stokes-like theorem. This result constitutes a geometric view of programming where data are handled like fields in physics.

Vérification de la redécoration pour des matrices triangulaires infinies en Coq

Ralph Matthes (IRIT)

Finite triangular matrices with a dedicated type for the diagonal elements can be profitably represented by a nested data type, i.e., a heterogeneous family of inductive data types, while infinite triangular matrices form an example of a nested coinductive type, which is a heterogeneous family of coinductive data types. Both kinds of families are fully supported since the version 8.1 of the Coq theorem proving environment, released in 2007. Reasoning about nested coinductive types naturally rests on observational equality, and the beta release of version 8.2 of Coq greatly helps in using the rewrite mechanism for Leibniz equality also for the notion of bisimilarity of infinite triangular matrices. With respect to that notion of equality, redecoration is shown to form a comonad. The main result, however, shows how to obtain redecoration through a redecoration algorithm on infinite streams of finite lists that does not involve the nested coinductive type. These new results come with a full formalization in Coq, and limitations of what Coq recognizes as a guarded definition make the theoretical development more challenging.

Un générateur de conditions de vérifications certifié pour un bytecode

Frédéric Besson (IRISA)

Nous avons spécifié et prouvé en Coq un générateur de conditions de vérifications (VCGen) qui adapte les algorithmes efficaces de Flanagan et Saxe [Flanagan et Saxe, Popl'01]. Pour valider l'approche, nous avons prouvé la correction sémantique d'un VCGen qui assure qu'un programme bytecode ne génère pas d'exception ArrayOutOfBound. Les conditions de vérifications sont abstraites à la volée et déchargées par un vérification réflexif de preuves arithmétiques. Le VCGen s'exécute efficacement en Coq. Ce travail ouvre la voie à une infrastructure PCC certifiée en Coq.

Interaction avec un gestionnaire de mémoire automatique

Zaynah Dargaye (CEDRIC et INRIA Rocquencourt)

Dans le cadre du développement et de la certification d'un compilateur optimisant pour un langage fonctionnel, nous avons spécifié et certifié en Coq l'interaction entre les programmes générés et un gestionnaire de mémoire automatique. Cette interaction nécessite deux passes de compilation. Chaque passe est une transformation vers un langage fonctionel intermédiaire. Le premier langage est propice au calcul des racines, le second explicite l'ensemble des racines. Cet exposé décrit la vérification formelle de ces deux transformations.

Scalable BIBOP garbage collection for parallel functional programs on multi-core machines

Luca Saiu (LIPN)

Exploiting modern multi-core processors requires task-parallel programs which are simply too hard to implement with traditional techniques; as high-level languages rely on automatic memory management subsystems, such subsystems must be made fast and scalable, tuned for today's complex memory architectures. I describe my implementation of a new parallel non-moving garbage collector for shared-memory machines, based on a variant of the BIBOP organization. Building on the experience of Boehm's work and revisiting some older ideas in the light of current hardware performance trends, I propose several improvements leading to compact data representation and measurable speedups, particularly in the context of functional programs. While discussing in detail the performance-critical sections of the implementation I provide an intuitive justification for my choices, corroborated with some measurements: allocation-heavy benchmarks average a scalability of 7.41 on eight cores. This effort results in a particularly clean architecture based on just a few data structures, which lends itself to experimentation with alternative techniques.

ENSIIE, 1 square de la résistance, 91 025 Évry cedex, France.
01 69 36 73 47.