wiki:Journees_LLL

Journées communes LTP - LAC - LAMHA

Le programme en pdf

Date et lieu

Jeudi 25 (après-midi) et Vendredi 26 octobre 2012, avec un tutoriel Isabelle/HOL le 24 et 25 (matin) octobre

LIFO, Orléans (comment venir)

Objectifs

Les groupes de travail LTP (Langages, Types et Preuves) et LaMHA (Langages et Modèles de Haut niveau pour la programmation parallèle, distribuée, de grilles de calcul et Applications) du GDR GPL et LAC (Logique Algèbre et Calcul) du GDR IM (Informatique Mathématique) tiendront une réunion commune à l'université d'Orléans les 25 et 26 octobre 2012.

Cette réunion permettra aux différents participants de ces groupes de travail de partager des idées et de présenter des travaux en cours. Elle se tiendra sur une journée et demi. Il n'y aura pas de frais d'inscription, mais les frais d'hébergement et de repas du soir seront à la charge des participants.

Planning

24 octobre 2012

Tutoriel Isabelle/HOL.

Une réservation a été faite pour le dîner à La Vieille Auberge (à la charge des participants). Carte pour s'y rendre depuis la Gare d'Orléans

25 octobre 2012

Matin

Suite du Tutoriel Isabelle/HOL.

Après-Midi

Demi-journée commune aux trois groupes de travail (Amphithéâtre Herbrand)

  • 14h00-15h00 : Daniel Hirschkoff, Calculs de processus: comportements, types, dualité
    Une première partie de cet exposé sera consacrée à une introduction au pi-calcul. Je présenterai le formalisme, en indiquant comment l'on peut s'en servir pour, d'une part, spécifier le comportement de systèmes concurrents, et, d'autre part, établir des équivalences entre de tels systèmes. J'évoquerai aussi des systèmes de types qui permettent de contrôler les interactions entre processus en pi-calcul. Dans la seconde partie de l'exposé, je présenterai une étude de la dualité entre émissions et réceptions en pi-calcul. Je montrerai comment une telle propriété peut être mise en avant en pi-calcul, et en quoi elle se peut s'avérer utile pour raisonner sur les processus. Il s'agit d'un travail en commun avec Jean-Marie Madiot et Davide Sangiorgi.
  • 15h00-15h30 : pause
  • 15h30-17h30 : exposés communs LAC - LTP - LaMHA (40 minutes par exposé). Exposés les plus susceptibles de susciter l'intérêt des différents groupes de travail.
  • Micaela Mayero (LIPN, Université Paris 13), Refléxions sur les réels de Coq
    (Travail commun avec Milad Niqui) Il existe plusieurs bibliothèques de nombres réels dans Coq. Deux d'entre elles, CoRN and Reals, sont très utilisées. L'une est intuitionniste et l'autre "plutôt classique". Nous exposerons les réflexions menées dans le but d'une librairie unifiée, dans le sens où aussi bien les utilisateurs de l'analyse classique que intuitionniste pourraient utiliser la même base. Nous commencerons par donner une description de ces deux bibliothèques en pointant les problèmes théoriques majeurs, puis, nous exposerons les débuts de réflexions réalisés dans une perspective d'unification.
  • Xavier Leroy (INRIA Rocquencourt, Gallium), Compilation vérifiée de l'arithmétique en virgule flottante
    L'arithmétique en virgule flottante joue un rôle essentiel dans de nombreux logiciels, mais présente de nombreux "pièges" tant pour le programmeur que pour l'auteur de compilateurs. La bibliothèque Flocq de Sylvie Boldo et Guillaume Melquiond offre une formalisation Coq très précise et complète de la norme IEEE-754 pour l'arithmétique en virgule flottante, et a déjà permis la vérification formelle de plusieurs algorithmes "flottants" subtils. Dans cet exposé, après un bref tutoriel sur l'arithmétique flottante et ses difficultés, j'expliquerai comment nous avons étendu et intégré Flocq dans le compilateur formellement vérifié CompCert afin de prouver la préservation de la sémantique IEEE-754 des calculs flottants tout au long de la compilation. (Travail joint avec Sylvie Boldo, Jacques-Henri Jourdan et Guillaume Melquiond).
  • Burkhart Wolff (LRI, Université Paris Sud), Parallelizing Interactive Theorem Provers: Challenges, Foundations and First Results
    This talk reports on first results of the ANR Paral-ITP Project targeting on pervasive parallelizing highly-trusted interactive theorem-provers, namely Coq and Isabelle. The talk covers different aspects of the parallelized prover architectures, namely computational structures, trusted LCF-Kernels and components, and new, IDE-like user-interfaces trying to give the user access to the underlying machinery. The talk reports on first results of the project and is of wider interest for parallel symbolic computation environments.

Dîner

Une réservation a été faite à La Chancellerie (à la charge des participants). Carte pour s'y rendre depuis l'arrêt de tramway, "Place de Gaulle".

26 octobre 2012

Programme

Exposé Invité

Francesco Zappa Nardelli (INRIA), Shared memory: reasoning in the muddle of programming languages and architectures
Optimisations performed by the hardware or by high-level language compilers can reorder memory accesses in various subtle ways. These reorderings can sometimes be observed by concurrent programs, exacerbating the usual problems of concurrent programming. In this talk will give an overview of relaxed memory models, both at the hardware level (with excerpts of the Intel x86 and IBM Power/ARM architectures) and at the high-level language level (with excerpts of the Java the C11/C++11 standard). I will then present some research projects my colleagues and I have worked on, ranging from proof of sample compilation schemes, to full verification of compiler optimisations, to random testing of widely-used compilers, highlighting the importance of the appropriate tool support for semantics, from proof assistants to ad hoc domain-specific languages.

Exposés

  • Catherine Lelay (INRIA Saclay Île-de-France), Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives
    Verification of numerical analysis programs requires dealing with derivatives and integrals. High confidence in this process can be achieved using a formal proof checker, such as Coq. Its standard library provides an axiomatization of real numbers and various lemmas about real analysis, which may be used for this purpose. Unfortunately, its definitions of derivative and integral are unpractical as they are partial functions that demand a proof term. This proof term makes the handling of mathematical formulas cumbersome and does not conform to traditional analysis. Other proof assistants usually do not suffer from this issue; for instance, they may rely on Hilbert's epsilon to get total operators. In this paper, we propose a way to define total operators for derivative and integral without having to extend Coq's standard axiomatization of real numbers. We proved the compatibility of our definitions with the standard library's in order to leverage existing results. We also greatly improved automation for real analysis proofs that use Coq standard definitions. We exercised our approach on lemmas involving iterated partial derivatives and differentiation under the integral sign, that were missing from the formal proof of a numerical program solving the wave equation.
  • Yann Salmon (IRISA, Université Rennes 1), Atteignabilité pour les systèmes de réécriture avec stratégies
    Nous cherchons à calculer des sur-approximations régulières d'ensembles de termes atteignables par un système de réécriture appliqué avec une stratégie. Actuellement, nous travaillons à adapter la complétion équationnelle d'automates d'arbres aux stratégies en profondeur, qui sont les stratégies d'évaluation de nombreux langages fonctionnels comme OCaml. L'objectif est de fournir au programmeur des informations de types de fonctions plus riches que celles fournies par les compilateurs existants.
  • Hélène Coullon (LIFO, Université d'Orléans), SkelGIS a new hierarchical library of algorithm skeletons
    La plupart des domaines scientifiques actuels disposent d'une quantité de données à traiter de plus en plus importante, posant des problèmes de chargement mais également de calculs sur des machines standard. Cela fait émerger dans beaucoup de domaines scientifiques un fort besoin non seulement en calcul parallèle mais également en distribution de données. Les librairies de squelettes de programmation parallèle cherchent à proposer une programmation séquentielle à l'utilisateur, tout en lui masquant l'aspect parallèle et complexe qui se cache derrière leur utilisation. Toutefois nous montrerons que l'approche systématique par éléments, induit de fortes limitations sur les librairies existantes pour le calcul sur matrices à deux dimensions, et notamment sur de gros volumes de données. Nous présentons dans cet article une nouvelle approche, par blocs, de squelettes de programmation parallèle sur des structures de données distribuées à deux dimensions.
  • Frédéric Gava (LACL, UPEC), Mechanised deductive verification of sequential and distributed state-space algorithms
    Explicit model-checking (MC) is a classical solution to find flaws in a security protocol. But it is well-known that for non trivial protocols, MC may enumerate state-spaces of astronomical sizes --- the famous state-space explosion problem. Distributed model checking is a solution but complex and subject to bugs: a MC can validate a model but miss an invalid state. In this paper, we focus on using a verification condition generator that takes annotated distributed algorithms and ensures their termination and correctness. We study seven algorithms (three sequential and four distributed where three of them are dedicated and optimised for security protocol) of state-space construction as a first step towards mechanised verification of distributed model-checkers.
  • Ludovic Henrio (CNRS, Sophia-Antipolis), Behavioural specification and verification of GCM component
    The objective of our work on behavioural specification is to verify the correct behaviour of applications made of asynchronous (GCM) components. We used pNets to build behavioural models of distributed applications of increasing size and complexity. Overall we are now at a state where, from an abstract specification of the service methods of individual components, we are able to build a finite model of the behaviour of a complete GCM application and to check its properties using model-checking tools. This talk will show some of the features we are able to model and some of the use-cases we were able to verify
  • Ludovic Henrio (CNRS, Sophia-Antipolis), Multi-active objects
    The active object programming model is particularly adapted to easily program distributed objects: it separates objects into several activities, each manipulated by a single thread, preventing data races. However, this programming model has its limitations in terms of expressiveness -- risk of deadlocks -- and of efficiency on multicore machines. To overcome these limitations, we propose an extension of the active object model, called multi-active objects, that allows each activity to be multithreaded. The new model is implemented as a Java library and relies on method annotations to decide which requests can be run in parallel. It provides implicit parallelism, sparing the programmer from low-level concurrency mechanisms. We define the operational semantics of the multi-active objects and study the basic properties of this model. The benefits of our proposal are highlighted using two different applications: the NAS Parallel Benchmarks and a peer-to-peer overlay.
  • Kento Emoto (The University of Tokyo), Generate, Test, and Aggregate - A Calculation-based Framework for Systematic Parallel Programming with MapReduce
    MapReduce, being inspired by the map and reduce primitives available in many functional languages, is the de facto standard for large scale data-intensive parallel programming. Although it has succeeded in popularizing the use of the two primitives for hiding the details of parallel computation, little effort has been made to emphasize the programming methodology behind, which has been intensively studied in the functional programming and program calculation fields. We show that MapReduce can be equipped with a programming theory in calculational form. By integrating the generate-and-test programing paradigm and semirings for aggregation of results, we propose a novel parallel programming framework for MapReduce. The framework consists of two important calculation theorems: the shortcut fusion theorem of semiring homomorphisms bridges the gap between specifications and efficient implementations, and the filter-embedding theorem helps to develop parallel programs in a systematic and incremental way. We give nontrivial examples that demonstrate how to apply our framework.
  • Matin Musicante (Federal University of Rio Grande do Norte), Automatic Refinement of Service Compositions
    We propose a method for the automatic composition of processing units (i.e., web services or components). Our method uses query rewriting techniques to translate high-level specifications into lower-level ones. We consider both functional and non-functional requirements. We extend and adapt the MiniCon query rewriting algorithm to obtain a specification refinement algorithm which takes into account the existence of an ontology alignment, optional parameters and conversion functions. Experiments indicate that our method produces feasible compositions.
  • Andre Oliveira Maroneze (IRISA, INRIA Rennes), Certification d'une analyse de bornes de boucles pour le WCET
    Dans le cadre de l'estimation du temps d'exécution au pire cas (WCET) pour les systèmes temps-réel, nous nous intéressons à certifier formellement (à l'aide de Coq) ne méthode d'estimation de bornes de boucles. Cette méthode est intégrée au compilateur C CompCert, pour une utilisation postérieure par des outils de calcul de WCET.
  • Sébastien Limet (LIFO, Université d'Orléans), Un modèle pour la composition d'applications de visualisation et d'interaction continue avec des simulations scientifiques
    La simulation informatique est un outil incontournable dans les sciences expérimentales. La puissance de calcul croissante des ordinateurs associée au parallélisme et aux avancées dans la modélisation mathématique des phénomènes physiques permet de réaliser virtuellement des expériences de plus en plus complexes. De plus, l'émergence de la programmation GPU a considérablement accru la qualité et la rapidité de l'affichage. Ceci a permis de démocratiser la visualisation sous forme graphique des résultats de simulation. La visualisation scientifique peut être passive : l'utilisateur peut suivre l'évolution de la simulation ou bien observer ses résultats après que le calcul soit terminé. Elle peut aussi être interactive lorsque le chercheur peut agir sur la simulation alors qu'elle se déroule. Créer de telles applications complexes n'est cependant pas à la portée de tout scientifique non informaticien. La programmation par composants est, depuis des années, mise en avant comme une solution à ce problème. Elle consiste à construire des applications en interconnectant des programmes exécutant des tâches élémentaires. Notre modèle de composants associé à une méthode de composition d'applications de visualisation scientifique interactive s'intéresse à la conciliation de deux contraintes majeures dans la coordination de ces applications : la performance et la cohérence.
  • Philippe Wang (LIP6, UPMC), Couverture de code structurelle pour OCaml pour la qualification d'un outil de développement
    Les outils de développement pour les logiciels critiques doivent passer le processus de "qualification". Développer un outil (e.g. un compilateur) qui produit du code critique impose la qualification de cet outil pour lequel il faut notamment établir différentes mesures de couverture de code. La mesure de couverture de code structurelle fait partie des documents issus des activités de test et vérification du cycle de développement. Le critère MC/DC (modified condition/decision coverage) s'intéresse de près aux conditions et aux décisions présentes dans un programme. Cet exposé propose une définition formelle des notions de condition et décision pour un langage ML puis un outil de couverture de code (Zamcov) implantant cela pour le langage OCaml.
  • Arnaud Jobin (IRISA, ENS Cachan), Inférence d'invariants polynomiaux
    Nous proposons une analyse statique pour calculer des invariants polynomiaux pour des programmes impératifs. L'analyse est issue de l'interprétation abstraite d'une sémantique arrière et effectue un calcul de préconditions assurant que des égalités du type g=0 sont vérifiées à la fin du programme. Une particularité importante de notre technique est qu'elle permet le calcul d'invariants de boucles polynomiaux sans avoir à effectuer de calculs de bases de Gröbner. Afin de traiter efficacement les conditionnelles et les boucles, l'analyse utilise des calculs de restes sur des polynômes paramétrés. L'algorithme peut analyser et trouver la majorité des invariants de boucle présents dans la littérature et s'exécute significativement plus vite que les implémentations utilisant les bases de Gröbner.
  • Thibaut Balabonski (INRIA Rocquencourt), Le sens du partage
    Le partage, ou la mémorisation de résultats intermédiaires, ajoute des « raccourcis » à l'espace de réduction d'un programme. On pourrait penser que ces raccourcis permettent d'arriver plus vite au résultat. Ce n'est cependant pas tout à fait exact. Nous montrerons en effet que dans le cadre de la « réduction faible », qui donne une bonne approximation des stratégies de réduction que l'on sait mettre en œuvre simplement, les réductions optimales avec ou sans partage ont même longueur. En revanche, toujours en réduction faible, nous verrons que sans partage ces stratégies optimales ne peuvent pas être calculables, alors qu'avec partage il existe des stratégies optimales très simples, à commencer par « l'appel par nécessité » de Wadsworth. Le partage ne modifie donc pas la borne inférieure. Il la rend accessible.
  • Chantal Keller (INRIA, Ecole Polytechnique) Parametricity in an Impredicative Sort
    Reynold's abstraction theorem is now a well-established result for a large class of type systems. In this talk, I will investigate Reynold's parametricity for the Calculus of Inductive Constructions (CIC), the underlying formal language of Coq. I will first present some possible benefits from having parametricity in a system like Coq, which are both theoretical (proving the independence of propositions with respect to the logical system) as well as practical (proving properties about finite algebraic structures). I will then explain the foundations of this work, which consist in defining a close refinement of CIC in which all terms are parametric.
  • Olivier Hermant (MINES ParisTech) Dedukti: A Universal Proof-Checker
    we introduce Dedukti, a proof-checker implementing the lambda-Pi calculus modulo, and that is developed at INRIA Paris-Rocquencourt. Its versatility allows it to check proofs coming from various formats, for instance Coq or Isabelle/HOL via OpenTheory. We also introduce the encoding tools.
  • Alain Giorgetti (Institut Femto-ST) Automatic Decidability Modulo Theories by Schematic Superposition
    Decision procedures for satisfiability modulo background theories of classical datatypes such as lists or arrays are at the core of many state-of-the-art verification tools. Using the superposition calculus for equational reasoning helps the researcher designing and implementing satisfiability procedures in a flexible way. Schematic superposition, in turn, provides a mean to reason on the derivations computed by superposition. We present the first implementation of schematic superposition and its extension to a fragment of arithmetics, namely the theory of Integer Offsets. We also show how it automatically provides decidability proofs for some theories of practical use.
  • Ali Assaf (INRIA, Ecole Polytechnique) Translating HOL to Dedukti
    Current proof systems (Coq, HOL, etc.) suffer from a lack of interoperability. It is currently very hard to transfer a theory from one system to the other. To solve this problem, we can express the theories in a common proof framework called Dedukti. This framework is based on the lambda-Pi calculus modulo, a language which is simple yet flexible enough to express theories coming from a variety of proof systems. In this presentation, I will show how we can express the theorems of HOL in the lambda-Pi calculus modulo in a sound and complete manner. I will then present the results of translating the HOL standard library to Dedukti.
  • Chong Li (LACL, UPEC & EXQIM) Implementation of data-parallel skeletons using SGL model
    Writing parallel programs is known to be notoriously dicult. Often programmers do not want to reason about message-passing algorithms and only want to combine existing high-level patterns to produce their parallel program. This is the algorithmic skeletons approach to parallel programming. It improves reliability and clarity of source code. But skeletons can be insucient when complicated communication schemes are needed. Expressing skeletons in a more general and low level language in the form of a library seems to be a good compromise between simplicity and expressive power. We present here a coarse-grained implementation using a hierarchical model of a set of data-parallel skeletons.
  • Thomas Pinsard (LIFO, Université d'Orléans) Operational Semantics of a Programming Language with Nested Transactions
    Programming concurrency systems with shared memory is notoriously difficult. Traditionally to protect the code from interferences, programmers use locks, and need a good understanding of the whole program. An other way, is to let only the programmer identify atomic sections, ie the portion of code that must be protected, and leave the responsibility for ensuring this property. To achieve a good modularity it is important that atomic sections support nesting. We propose an operational semantics of a programming language with nested atomic sections, and define notions of well-synchronised programs, and atomicity on traces of an execution. We show that well-synchronised programs ensure atomicity.
  • Alexis Bernadet (LIX, Ecole Polytechnique), A big-step operational semantics via non-idempotent intersection types
    We introduce a typing system of non-idempotent intersection types that characterizes strongly normalising lambda-terms and such that a trivial measure on the typing tree (used to prove strong normalisation) is equal to the length of the longest β-reduction sequence. Moreover, the type of a term gives us the structure of the normal form. Therefore, a typing system can be viewed as a derivation in a big-step operational semantics.
  • Dalia Kesner (PPS, Université Denis Diderot) Normalisation for Dynamic Pattern Calculi
    The Pure Pattern Calculus (PPC) extends the lambda-calculus, as well as the family of algebraic pattern calculi, with first-class patterns i.e. patterns can be passed as arguments, evaluated and returned as results. The notion of matching failure of the PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies the calculus with parallel-or-like, non-sequential behaviour. Therefore, devising normalising strategies for the PPC to obtain well-behaved implementations turns out to be challenging. This talk will first introduce the Pure Pattern Calculus, then will focus on normalising reduction strategies for PPC. We will describe a (multistep) strategy which is normalising. The proof is based on the notion of necessary set of redexes, a generalisation of the notion of needed redex encompassing non-sequential reduction systems.
  • Sergueï Lenglet (Université de Lorraine) Bisimulations pour les opérateurs de contrôle délimité
    Les opérateurs de contrôle délimité permettent à un programme d'avoir accès et de manipuler une partie du contexte d'exécution. Ainsi, l'opérateur shift permet de sauvegarder une partie du contexte (délimité par reset) pour un usage futur. Nous définirons dans cet exposé une équivalence comportementale pour un lambda-calcul étendu avec shift/reset, et nous verrons comment prouver des équivalences de termes à l'aide de bisimulations.
  • Guillaume Baudard (INRIA, ENS) Interprétation synchrone d'un langage d'intéraction pour la musique mixte
    Dans le cadre de la musique dite mixte, le langage d’Antescofo permet de spécifier conjointement parties électroniques et parties instrumentales. L’ordinateur, peut ainsi au moment de la performance, être considéré comme un musicien qui interagit avec les autres instrumentistes. En ce sens, une partition Antescofo permet de spécifier un système réactif particulier : une performance musicale. L'objectif de ce travail est d'utiliser l'expressivité temporelle d'un langage synchrone réactif tel que Reactive ML pour interpréter les différentes structures de contrôle offertes par le langage d'antescofo au plus près de leurs spécifications. L'utilisation de Reactive ML, langage pourvu d'une sémantique bien définie, permet en outre de munir ces structures d'une sémantique par traduction.
  • Catherine Dubois (Cédric, ENSIIE), A Certified Constraint Solver over Finite Domains
    Constraint programs such as those written in modern Constraint Programming languages and platforms aim at solving problems coming from optimization, scheduling, planning, etc. Recently CP programs have been used in business-critical or safety-critical areas as well, e.g., e-Commerce, air-traffic control applications, or software verification. This implies a more skeptical regard on the implementation of constraint solvers, especially when the result is that a constraint problem has no solution, i.e., unsatisfiability. In this talk, we present a Coq formalisation of a well-known constraint filtering algorithm — AC3 — and a simple labeling procedure. The proof of their soundness and completeness has been completed using Coq. As a result, a formally certified constraint solver written in OCaml has been automatically extracted from the Coq specification of the filtering and labeling algorithms. The solver, yet not as efficient as specialized existing (unsafe) implementations, can be used to formally certify that a constraint system is unsatisfiable.

Hôtels

Here is a list of some recommended hotels in the city center:

Main hotels are listed here. You can also have a look at the list of hotels compiled by the tourism information desk.

Comité d'organisation

  • Frédéric Loulergue (LIFO, Université d'Orléans)
  • Wadoud Bousdira (LIFO, Université d'Orléans)
  • Hélène Coullon (LIFO, Université d'Orléans)
  • Sylvain Jubertie (LIFO, Université d'Orléans)
  • Florence Maubert (Université d'Orléans)
  • Thomas Pinsard (LIFO, Université d'Orléans)
  • Isabelle Renard (LIFO, Université d'Orléans)
  • Julien Tesson (LACL, Université Paris Est)

et les responsables des groupes de travail

Last modified 2 years ago Last modified on Oct 23, 2012, 12:23:32 PM

Attachments (2)

Download all attachments as: .zip