Groupe de travail LTP du GDR GPL

28 novembre 2016

PCRI (bâtiment Ada Lovelace - 650), Université Paris-Sud

Salle 435 (salle des thèses)

Cette réunion permettra aux différents participants du groupe de travail de partager des idées et de présenter des travaux aboutis ou en cours. Cette année, nous invitons les étudiants à présenter leur résultats de stage de M2 ou de début de thèse, dans un exposé court (15 min).

Comment venir

Informations pratiques pour venir au PCRI

Programme

09:30	Accueil
09:45	My Taylor is rich, Xavier Thirioux (ENSEEIHT/IRIT)
	Nous présentons nos travaux portant sur la définition d'une algèbre des séries de Taylor en OCAML, dont une application, parmi tant d'autres, est la vérification de contrôleurs dans le domaine des systèmes embarqués. En effet, les séries de Taylor fournissent des approximations polynomiales de toute expression numérique, expression apparaissant dans les lois de commandes mais également dans les invariants sur le comportement de ces lois. Bien que les séries de Taylor soient depuis longtemps utilisées et intégrées dans de nombreux outils, notre approche est innovante par plusieurs aspects: séries multi-dimensionnelles avec algèbre de tenseurs symétriques sous-jacente; séries construites incrémentalement, dont l'ordre du développement peut être augmenté dynamiquement; calcul d'une erreur certifiée (en plus du développement polynomial) par approximation du reste de Taylor; implémentation soignée pour freiner l'explosion combinatoire; accent mis sur la correction de l'implémentation, notamment par un usage massif des GADT et de l'arithmétique au niveau des types; algèbre complète, incluant l'arithmétique, les fonctions élémentaires et les opérateurs intégraux et différentiels, permettant la résolution de PDE directement par construction d'une valeur récursive. Nous présentons également les possibilités de calcul offertes sur un exemple de contrôleur et abordons les nombreuses perspectives ouvertes par ces travaux.
10:30	Programmation d'algorithmes multi-BSP en ML: Multi-ML et son typage, Victor ALLOMBERT (Paris Est)
	Le modèle Multi-BSP, extension du modèle de parallélisme quasi-synchrone BSP, propose une représentation des machines hiérarchique sous la forme d'un arbre de mémoires et de processeurs. En s'appuyant sur ce modèle, nous proposons le langage Multi-ML conçu pour programmer des algorithmes adaptés à ces machines hiérarchiques. Le langage Multi-ML est basé sur BSML (Bulk Synchronous Parallel ML), un langage fonctionnel pour la programmation d'algorithmes BSP. Nous présenterons les principaux concepts du langage Multi-BSML et son système de types "à la ML" avec des annotations supplémentaires de localité (effets) sur les types permettant de mettre en évidence le placement des données dans la hiérarchie des mémoires.
10:55	PAUSE
11:15	Permissions en lecture seule temporaires en logique de séparation, François Pottier (INRIA)
	Je présenterai une extension de la logique de séparation (séquentielle) avec un mécanisme général qui permet de convertir temporairement n'importe quelle assertion (ou "permission") en une forme qui donne accès en lecture seule. Aucun comptage (entier ou fractionnel) n'est nécessaire: les permissions en lecture seule peuvent être dupliquées ou jetées sans restriction. Nous pensons que, dans certaines circonstances où on souhaite accéder en lecture seule à une structure de données modifiable, les permissions en lecture seule permettent des spécifications et des preuves plus concises. La méta-théorie de cette proposition a été vérifiée en Coq. (Travail commun avec Arthur Charguéraud.)
11:40	The Matrix Reproved, Martin CLOCHARD (Université Paris Sud / LRI)
	we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version using three nested loops and the Strassen's algorithm. The proofs are conducted using the Why3 platform for deductive program verification, and automated theorem provers to discharge proof obligations. In order to specify and prove the two multiplication algorithms, we develop a new Why3 theory of matrices and apply the proof by reflection methodology.
11:55	Typer les flux multimedia dans Antescofo, Pierre DONAT-BOUILLUD (IRCAM)
	Une extension récente d'Antescofo, un langage dédié pour les interactions musicales, permet de traiter des flux de données, par exemple audio, caractérisés par une période et un nombre d'échantillons traités à chaque période. Ces traitements, décrits de manière fonctionnelle, peuvent se reconfigurer dynamiquement, et sont externes et décrits par d'autres DSLs comme Faust. Notre travail actuel vise à décrire un système de types permettant d'analyser l'ordonnancement de ces traitements, pour améliorer la précision temporelle entre flux audio et flux de contrôle, et à composer des traitements hétérogènes en terme de période et d'échantillons.
12:10	Expliquer les différences de programmes à l'aide d'oracles, Thibaut Girka (IRIF)
	La comparaison de programmes et la description de leurs différences sont des problématiques omniprésentes en développement logiciel, mais la plupart des représentations utilisées pour ces différences sont textuelles, peu structurées, et ne prend pas en compte l'aspect sémantique des modifications. Nous présentons un cadre formel permettant de caractériser des différences d'exécution à petit pas entre programmes déterministes. Ce cadre définit une notion de langages de différences, dans lesquels des oracles-programmes mettant en relation les exécutions à petit pas d'autres programmes d'un même langage peuvent être écrits, et sur lesquels on peut raisonner. Dans cet exposé, nous illustrerons ce cadre par quelques exemples de différences sur le langage impératif minimal Imp.
12:25	DÉJEUNER
14:00	Une preuve formelle de l'algorithme de Tarjan (1972) pour trouver les composantes fortement connexes dans un graphe., Jean-Jacques Lévy (INRIA / IRIF)
	Nous présentons une preuve formelle de l'algorithme de Tarjan (1972) pour trouver les composantes fortement connexes dans un graphe. Cet algorithme exécute une seule passe sur le graphe le parcourant en profondeur d'abord. Notre programme est ici écrit dans un style de programmation fonctionnelle dans le langage Why3-ML. La preuve utilise des lemmes et des assertions exprimés dans la logique de Why3. La majorité d'entre eux sont prouvés automatiquement à l'exception de 5 assertions ou lemmes prouvés manuellement en Coq. Une preuve d'une version impérative de ce programme ne figure pas dans ce travail, mais nous indiquons comment y parvenir par raffinements successifs. Un point important est que nos preuves sont intuitives, publiables et lisibles par un humain. Co-auteur Ran Chen, Iscas Pékin et Inria Saclay. Travail présenté à JFLA, 2017
14:45	jsCoq: Towards Hybrid Theorem Proving Interfaces, Pierre JOUVELOT (MINES ParisTech)
15:10	PAUSE
15:30	Structural analysis of trivalent maps, formally, Alain GIORGETTI (Institut FEMTO-ST)
	Rooted trivalent maps are known to be in one-to-one correspondence with closed linear lambda terms. As a step towards a mechanized proof of this correspondence we synthetize an inductive structure for rooted trivalent maps by composition of edge removals.
15:55	OCaLustre : une extension synchrone d'OCaml pour la programmation de microcontrôleurs, Steven VAROUMAS (UPMC)
	Les microcontrôleurs sont des circuits intégrés programmables destinés principalement au contrôle d'objets qui interagissent avec leur environnement. En effet, les programmes exécutés sur microcontrôleurs ont généralement pour rôle de lire des signaux électriques reçus de la part des composants auxquels ils sont branchés (boutons, capteurs, ...) et d'émettre des signaux à divers effecteurs (LED, résistances, écrans, ...). La programmation synchrone à flots de données semble alors particulièrement adaptée au développement de tels systèmes. Nous proposons OCaLustre : une extension du langage multi-paradigmes OCaml qui introduit la notion de noeuds synchrones inspirée du langage Lustre. Destinée à être exécutée sur des microcontrôleurs aux capacités mémoires limitées, OCaLustre tire profit de la machine virtuelle OCaPIC permettant l'exécution de code-octet OCaml sur des microcontrôleurs PIC 18F.
16:10	Conception et implantation en Ocaml d'un traducteur de Lustre vers Promela, et vérification formelle de programmes exemples avec le model-checker SPIN, Samuel RISBOURG (CEA)
	Lustre est un langage de programmation synchrone, à flot de données et défini formellement, destiné à la conception de systèmes réactifs. Le model checking est une méthode formelle permettant d'analyser exhaustivement le comportement de programmes lors de leur exécution. Ce rapport présente le travail effectué du mois d'avril au mois de septembre 2016 au sein du CEDRIC, le laboratoire d'informatique du CNAM, durant mon stage du Master Systèmes Embarqués Mobiles et Sûrs (SEMS). L'objectif du stage était de traduire des programmes exemples écrits en Lustre en modèles Promela, le langage du model checker SPIN, et d'en vérifier les propriétés de sureté.
16:25	Génération du code certifié pour Lustre, Lélio BRUN (INRIA/ENS)
	Les compilateurs de langages schémas-blocs, comme Lustre ou Scade, utilisent souvent un langage intermédiaire entre le code flot de données source et le code impératif cible. Nous avons récemment implémenté et vérifié une fonction de traduction dans Coq d'un langage intermédiaire simple vers le langage Clight accepté par le compilateur CompCert. Le langage intermédiaire utilise une représentation idéalisée d'une mémoire hiérarchique, alors que Clight utilise un modèle de mémoire sophistiqué assez proche de la machine. Notre preuve de correction doit donc confronter les questions d'alignement, d'aliasing, et du padding. On se sert des prédicats de séparation développés dans CompCert pour résoudre ces problèmes.
16:40	PAUSE
17:00	Hybrid Information Flow Analysis for Real-World C Code, Gergö BARANY (CEA List)
	Information flow analysis models the propagation of data through a software system and can identify unintended information leaks. There is a wide range of such analyses, tracking flows statically, dynamically at run time, or in a hybrid way combining both static and dynamic approaches. We present a hybrid information flow analysis for a large subset of the C programming language. Extending previous work that handled a few difficult features of C, our analysis can deal with pointers, arrays, pointer arithmetic, structures, dynamic memory allocation, complex control flow, and statically resolvable indirect function calls. The analysis is implemented as a plugin to the Frama-C framework. We demonstrate the applicability and precision of our analyzer by applying it to an open-source cryptographic library. We verify an information flow policy that proves the absence of control-flow based timing attacks against the implementations of many common cryptographic algorithms. Conversely, we demonstrate that our analysis is able to detect a known instance of this kind of vulnerability in another cryptographic primitive.
17:25	Un point de vue de théorie des jeux sur la logique de séparation concurrente, Léo STÉFANESCO
17:50	Fin de LTP 2016

Participants

Sylvain CONCHON

Marc POUZET

Mario PEREIRA

Martin CLOCHARD

Léon GONDELMAN

Steven VAROUMAS

Jean-Christophe LÉCHENET

Boubacar SALL

Victor ALLOMBERT

Frédéric GAVA

Fatiha ZAÏDI

Rémy EL SIBAÏE

Xavier LEROY

Alain GIORGETTI

Viet Hoang LE

Timothy BOURKE

Lélio BRUN

Léo STÉFANESCO

Paul-André MELLIES

Thibaut GIRKA

Oliver HERMANT

Pierre DONAT-BOUILLUD

Samuel RISBOURG

Pierre-Evariste DAGAND

François POTTIER

Nikolay KOSMATOV

Gergö BARANY

Julien SIGNOLES

Catherine DUBOIS

Pierre JOUVELOT

Jean-Paul BODEVEIX

Jean-Christophe FILLIÂTRE

Jean-Jacques LÉVY

Xavier THIRIOUX

Julien TESSON

Armaël GUÉNEAU