JFLA 2021

Journées Francophones des Langages Applicatifs
Journées virtuelles
mercredi 7 avril 2021

vendredi 9 avril 2021
En ligne
En ligne

Les actes des JFLA 2021 sont téléchargeables depuis le lien ci-dessous.

Dates importantes

Soumission des résumés 1er octobre 2020
Soumission des articles 15 octobre 2020 8 octobre 2020
Notification aux auteurs 16 novembre 2020 9 novembre 2020
Clôture des inscriptions 3 avril 2021

Inscription

Pour effectuer votre inscription, veuillez suivre le lien ci-dessous, avant le samedi 3 avril 2021 :

S'inscrire aux JFLA

La situation sanitaire nous a contraint à organiser les JFLA 2021 en ligne. En conséquence, l’inscription sera gratuite cette année.

Pour s’inscrire, il suffit de remplir le formulaire dont le lien est donné ci-dessus

Nous espérons que vous serez nombreux à participer à ces journées. Inscrivez-vous dès que possible !

Programme

Cours invités

Loic Correnson (CEA List)
Pratique de la preuve de programme avec Frama-C/WP et Why-3

Exposés invités

David Mentré (Mitsubishi Electric R&D Centre Europe)
Some views on industrial usages of Formal Methods

En détails

mercredi 7 avril

  • 09:20 — 09:25
    Yann Régis-Gianas et Chantal Keller
    Lancement des JFLA virtuelles
  • 09:25 — 09:50
    Mário Pereira et António Ravara
    Cameleer: a Deductive Verification Tool for OCaml
  • 09:50 — 10:05
    Matthieu Journault , Antoine Miné , Raphaël Monat et Abdelraouf Ouadjaout
    Démonstration de la plateforme Mopsa d'analyse statique de programmes par interprétation abstraite
  • 10:20 — 10:45
    Frédéric Bour , Basile Clément et Gabriel Scherer
    Tail Modulo Cons
  • 10:45 — 11:00
    Thierry Martinez
    Type-safe type reflection for OCaml
  • 11:15 — 11:30
    Thomas Letan et Li Yao Xia
    coqffi: Génération automatique de FFI Coq-OCaml
  • 14:00 — 15:30
    Loic Correnson (CEA List)
    Pratique de la preuve de programme avec Frama-C/WP et Why-3

jeudi 8 avril

  • 09:00 — 09:25
    Quentin Ladeveze
    Preuve formelle de la propriété DRF-SC dans le modèle RC11
  • 09:25 — 09:50
    Adam Khayam , Louis Noizet et Alan Schmitt
    JSkel: Towards a Formalization of JavaScript’s Semantics
  • 09:50 — 10:15
    Timothy Bourke , Paul Jeanmaire , Basile Pesin et Marc Pouzet
    Normalisation vérifiée du langage Lustre
  • 10:30 — 10:55
    Julien Girard-Satabin , Aymeric Varasse , Guillaume Charpiat , Zakaria Chihani et Marc Schoenauer
    Partitionnement en régions linéaires pour la vérification formelle de réseaux de neurones
  • 10:55 — 11:10
    Jocelyn Sérot
    Lavez vos graphes plus blanc avec HoCL
  • 11:10 — 11:25
    Denis Merigoux et Raphaël Monat
    Mlang: an Open-Source Toolchain for the Income Tax Computation
  • 14:00 — 15:00
    David Mentré (Mitsubishi Electric R&D Centre Europe)
    Some views on industrial usages of Formal Methods
  • 15:00 — 16:00
    Loic Correnson (CEA List)
    Pratique de la preuve de programme avec Frama-C/WP et Why-3

vendredi 9 avril

  • 09:00 — 09:25
    Aïna Linn Georges , Armaël Guéneau , Thomas Van Strydonck , Amin Timany , Alix Trieu , Dominique Devriese et Lars Birkedal
    Cap' ou pas cap' ?
  • 09:25 — 09:50
    Xavier Denis
    Mastering Program Verification using Possession and Prophecies
  • 09:50 — 10:05
    Théo Laurent et Kenji Maillard
    Mettons de l'Ordre dans CIC !
  • 10:20 — 10:35
    Alain Giorgetti
    Théories de permutations avec Why3
  • 10:35 — 10:50
    Josué Moreau
    Les nombres premiers au crible de la preuve formelle
  • 10:50 — 11:05
    Érik Martin-Dorel et Pierre Roux
    Flottants primitifs dans Coq
  • 11:05 — 11:20
    Jocelyn Sérot et Emmanuel Chailloux
    OCaml sur circuit FPGA

Appel à soumission

Les 32es Journées Francophones des Langages Applicatifs (JFLA) se tiendront à Journées virtuelles, plus précisément En ligne , du mercredi 7 avril 2021 au vendredi 9 avril 2021 .

Les JFLA réunissent concepteurs, utilisateurs et théoriciens ; elles ont pour ambition de couvrir les domaines des langages applicatifs, de la preuve formelle, de la vérification de programmes, et des objets mathématiques qui sous-tendent ces outils. Ces domaines doivent être pris au sens large : nous souhaitons promouvoir les ponts entre les différentes thématiques.

  • Langages fonctionnels et applicatifs : sémantique, compilation, optimisation, typage, mesures, extensions par d'autres paradigmes.
  • Assistants de preuve : implémentation, nouvelles tactiques,  développements présentant un intérêt technique ou méthodologique.
  • Logique, correspondance de Curry-Howard, réalisabilité, extraction de programmes, modèles.
  • Spécification, prototypage, développements formels d'algorithmes.
  • Vérification de programmes ou de modèles, méthode déductive, interprétation abstraite, raffinement.
  • Utilisation industrielle des langages fonctionnels et applicatifs, ou des méthodes issues des preuves formelles, outils pour le web.

Les articles soumis aux JFLA sont relus par au moins deux personnes s'ils sont acceptés, trois personnes s'ils sont rejetés. Les critiques des relecteurs sont toujours bienveillantes et la plupart du temps encourageantes et constructives, même en cas de rejet.

Il n'y a donc pas de raison de ne pas soumettre aux JFLA !

Soumission

Nous acceptons quatre types de soumissions :

  • Article de recherche de seize pages au plus (hors bibliographie) , portant sur des travaux originaux. Nous acceptons des travaux en cours, pour lesquels l'aspect recherche n'est pas entièrement finalisé.
  • Article court de huit pages au plus (hors bibliographie) , pour rechercher de l'aide pour résoudre un problème particulier, ou reparler d'un papier déjà publié.
  • Proposition de tutoriel d'une page (hors bibliographie) exposant son intérêt et ses objectifs ainsi que l'environnement informatique nécessaire à sa réalisation.
  • Proposition de démonstration d'un outil ou d'un prototype de deux pages (hors bibliographie) décrivant pourquoi ce logiciel est intéressant ainsi que ses spécificités.

Dans tous les cas, la forme de l'article devra être soignée. Les articles sélectionnés seront publiés dans les actes de la conférence, et les auteurs seront invités à faire une présentation lors des journées, de vingt-cinq minutes pour les articles longs et de quinze minutes pour les courts. Les tutoriels auront un créneau de vingt-cinq minutes et les démonstrations d'outils ou de prototypes se verront allouer quinze minutes.

L'article peut être rédigé en anglais, auquel cas la présentation devra être effectuée en français. Néanmoins, dans le cas où il s'agit d'une republication au format court d'un article déjà publié, la publication doit être en français et la publication originale en anglais.

Le style LaTeX Easychair doit être respecté :

https://easychair.org/publications/for_authors

Les soumissions se font sur la page Easychair des JFLA :

https://easychair.org/conferences/?conf=jfla21

Organisation

Comité de programme

Yann Régis-Gianas Nomadic Labs Président
Chantal Keller LRI, Université Paris-Sud Vice-présidente
Timothy Bourke ENS
Evelyne Contejean LRI
Albin Coquereau OCamlPro
Claire Dross AdaCore
Adrien Guatto IRIF
Marie Kerjean Inria Rennes-Bretagne Atlantique
Pascale Le Gall CentraleSupelec
Rodolphe Lepigre MPI SWS
Thomas Letan ANSSI
Assia Mahboubi INRIA Nantes
Simão Melo de Sousa Universidade da Beira Interior
Damien Pous CNRS - ENS Lyon

Comité de pilotage

Zaynah Dargaye Nomadic Labs
Catherine Dubois École Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)
Jean-Christophe Filliâtre CNRS
Louis Mandel IBM Research
Micaela Mayero LIPN, Université Paris 13
Alan Schmitt Inria Rennes - Bretagne Atlantique
Julien Signoles CEA LIST
Pierre Weis Inria Paris