Journée LTP - Automne 2018

Co-localisée avec la journée MTV2

Cette page sera mise à jour régulièrement, n'hésitez pas à y revenir.

Date
jeudi 6 décembre 2018
Lieu
ENSIIE, Évry

Inscription avant le 19 novembre 2018

Cette journée est co-localisée avec la journée MTV2 (Méthodes de test pour la validation et la vérification), qui aura lieu le 7 décembre au même endroit.

Deux exposés invités seront présentés (résumés ci-dessous) :

Benoît Valiron (LRI/Modhel)
Calcul et langages de programmation quantique
Sylvain Boulmé (Laboratoire Verimag)
Embedding Impure ML Oracles into Coq Verified Code, Illustrated on SatAns-Cert, a Coq-Verified (Boolean) SAT-Solver.

Le GT LTP du GdR GPL :

Les thèmes du groupe de travail LTP (Langages, Types et Preuves) du GdR GPL sont :

Organisation

L'inscription à la journée est gratuite mais nécessaire pour assurer le bon déroulement de l'événement.

Le repas du midi n'est pas encore organisé, mais si tout se passe comme prévu, il sera financé par le GDR GPL.

Venir à l'ENSIIE

L'ENSIIE est facilement accessible depuis Paris Gare de Lyon ou Châtelet-Les halles via le RER D (gare d'Évry-Courcouronnes). Attention ne pas prendre les trains s'arrêtant à Évry Val de Seine, bien prendre ceux qui s'arrêtent à Évry-Courcouronnes. Sortez au bout du quai dans la direction du train. L'ENSIIE est ensuite fléchée.

Plus d'informations sur le site de l'ENSIIE.

Hôtels à proximité de l'ENSIIE (non testés, cette liste ne doit pas être considérée comme un soutien) :

Liste de participants

Présentations invitées

Sylvain Boulmé, Laboratoire Verimag

Embedding Impure ML Oracles into Coq Verified Code, Illustrated on SatAns-Cert, a Coq-Verified (Boolean) SAT-Solver.

Oracles are a key ingredient in the success of CompCert (an industrial C-Compiler which is formally verified in Coq). Such an oracle is an untrusted foreign code (written in OCaml) producing outputs that are checked by Coq-verified code. However, in CompCert, oracles are currently invoked through an unsafe FFI (Foreign Function Interface) of Coq. I will detail some pitfalls of this FFI and propose how to overcome them. Moreover, I conjecture that by using an adequate FFI, we can derive "theorems for free" a la Wadler in Coq from the ML type of imperative polymorphic oracles. This discharges a part of the proof effort on the OCaml typechecker. I will illustrate this idea on a few examples, including "SatAnsCert", a verified checker of boolean SAT-solvers.

Benoît Valiron, LRI/Modhel

Calcul et langages de programmation quantique

Dans cet exposé, je présenterai le calcul quantique, ses promesses, et l'état de l'art sur le front des langages de programmation quantique.

Programme

Le programme suivant est préliminaire, il est encore susceptible d'être modifié.

9h15-10h Accueil, café
10h00-11h15Session 1 (3x25min, 20 min exposé + 5 min questions)
LEDEIN Amélie, ENSIIE/Samovar. FaCiLe en Coq
ROBLES Virgile, CEA List, Laboratoire Sûreté et Sécurité des Logiciels. MetAcsl: Specification and Verification of High-Level Properties
RADANNE Gabriel, University of Freiburg. Kindly Bent to Free Us: Linear types for ML
11h15-11h40Pause café
11h40-12h30 Session 2 (conférencier invité)
Sylvain Boulmé (Laboratoire Verimag, Grenoble) : Embedding Impure ML Oracles into Coq Verified Code
12h30-14h00 Déjeuner
14h00-14h50 Session 3 (conférencier invité)
Benoît Valiron (LRI/Modhel, Paris Saclay) : Calcul et langages de programmation quantique
14h50-15h15 Pause café
15h15-16h55Session 4 (3x25min, 20 min exposé + 5 min questions)
MAGAUD Nicolas, ICUBE/IGG. Preuves sur des modèles finis de la géométrie projective
LEVILLAIN Olivier, Télécom SudParis. Parsifal: une solution pour écrire rapidement des parsers binaires robustes et efficaces
LY Dara, CEA List, Laboratoire Sûreté et Sécurité des Logiciels. Soundness of a Dataflow Analysis for Memory Monitoring
16h55-17h00 Annonces, fin de journée

Inscription

Envoyez votre inscription par e-mail à renaud.rioboo@ensiie.fr et guillaume.burel@ensiie.fr (cliquez ici, ou recopiez le bulletin ci-dessous) avant le 19 novembre.

Vous pouvez proposer des présentations de vos travaux sous la forme d'un exposé oral, d'un tutoriel, d'une démonstration d'outil, etc.

===================================
Nom :
Prénom :
Laboratoire/équipe :

[] je souhaite présenter des travaux.

 Titre et format de la présentation :

 Résumé (optionnel, à transmettre avant le 5/12) :

[] j'accepte que mes nom, prénom, équipe et éventuel titre de présentation
    apparaissent sur la page web de la journée, dès mon inscription.

[] je participerai au repas du midi.

 Pour le déjeuner, mes contraintes sont (végétarien, sans sel, ...) :

[] je participerai également à la journée MTV2 le lendemain.
   (pour information uniquement, l'inscription devra se faire des deux
    côtés.)

====================================

Résumés des présentations

Amélie LEDEIN, ENSIIE/Samovar

FaCiLe en Coq

La programmation par contraintes a pour objectif de résoudre des problèmes hautement combinatoires qui peuvent se modéliser sous la forme de la donnée d'un ensemble de variables ou d'inconnues munies chacune d'un domaine (c'est-à-dire l'ensemble des valeurs possibles) et d'un ensemble de contraintes sur ces variables. Différentes techniques de résolution de ces problèmes de satisfaction de contraintes ont été proposées et implantées dans des solveurs, Choco par exemple ou des bibliothèques spécialisées, la bibliothèque OCaml FaCiLe (Barnier, Brisset, 1997) par exemple. L'idée principale sous-jacente aux algorithmes de résolution est d'éliminer des domaines des variables, les valeurs qui ne peuvent figurer dans une solution du problème. La représentation d'un domaine peut différer d'un solveur à l'autre : listes d'intervalles, listes de "trous", ensembles, "bitvectors", etc. La bibliothèque FaCiLe, ainsi que de nombreux autres solveurs, implantent un domaine comme une liste d'intervalles. Nous avons traduit et vérifié formellement en Coq une grande partie du module de FaCiLe qui implante le type des domaines. Dans ce travail, l'effort s'est porté non seulement sur la preuve mais surtout sur la spécification des fonctions de ce module. Notre objectif à plus long terme est d'utiliser le module Coq correspondant dans le solveur de contraintes développé en Coq par Carlier et al, afin d'obtenir de meilleures performances. Ce travail participe à l'effort de vérifier en Coq les bibliothèques OCaml existantes

Olivier LEVILLAIN, Télécom SudParis

Parsifal: une solution pour écrire rapidement des parsers binaires robustes et efficaces

À venir.

Dara LY, CEA List, Laboratoire Sûreté et Sécurité des Logiciels

Soundness of a Dataflow Analysis for Memory Monitoring

An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g. their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.

Nicolas MAGAUD, ICUBE/IGG

Preuves sur des modèles finis de la géométrie projective

À venir.

Gabriel RADANNE, University of Freiburg

Kindly Bent to Free Us: Linear types for ML

À venir.

Virgile ROBLES, CEA List, Laboratoire Sûreté et Sécurité des Logiciels

MetAcsl: Specification and Verification of High-Level Properties

Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its specified contract. However, not all high-level (e.g.~security-related) properties of a software module can be easily expressed through function contracts. To address this issue, this tool demo paper proposes a new specification mechanism, called meta-properties, able to express a rich set of high-level properties. A meta-property can be seen as an enhanced global invariant specified for all or a subset of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can then be proved by deductive verification tools in a usual way. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove several safety- and security-related meta-properties in two illustrative case studies.