L'Agenda du Libre

Troisième événement du Printemps de l'innovation Open Source, organisé par le GTLL de Systematic et l'Irill, présidé par Roberto Di Cosmo

Langages et outils pour la fiabilité logicielle - Printemps de l'Innovation Open Source

Programme dirigé par Emmanuel Chailloux (LIP6/UPMC, Irill), Roberto Di Cosmo (Irif, Irill, Inria, UPD), Fabrice Le Fessant (Inria, OCamlPro)

 

• 14:00 - Introduction
• 14:15 - Coroutines: Adding cooperative multitasking to the Ada tasking model

  Raphaël Amiard, Adacore

  Ada was the first language to have standardized tasking in language semantics. However the collaboration model is not specified, and often implemented in terms of preemptive multitasking. In today's world where asynchronous programming models are very common, collaborative tasking is looking more and more interesting. I will present a prototype implementation adding such a model in Ada.

    bio : Raphaël Amiard, passionate about languages, semantics and compilers, joined AdaCore in 2013 to work on the IDE and on the compiler technologies. 

• 14:45 - Rust: Systems Programming for Everyone

  Léo Testard, Mozilla

  Rust is a new programming language that provides memory safety and data-race freedom while offering efficiency and low-level control comparable to that of C and C++. Rust allows for safe systems programming, including concurrent threads with shared data.
  I will describe the core concepts of the Rust language (ownership, borrowing, and lifetimes), as well as the tools beyond the compiler for open-source software component distribution (cargo).
  

  These pieces, along with the continued work of Rust's volunteer community, have led so-called "script programmers" to discover systems programming

  bio: Léo Testard is a research engineer at Mozilla, where he works on the Rust compiler, runtime libraries, and language design.

• 15:15 - Développement d'applications multi-plateformes Web et mobiles

  Vincent Balat, BeSport et Univ Paris Diderot

  Développer une application à la fois sur le Web et sur mobile demande la plupart du temps de multiplier les efforts, ce qui oblige les petites entreprises à faire des choix : se concentrer sur la version Web ou mobile, voire sur une seule plateforme mobile. Ocsigen permet aujourd'hui de développer des applications qui pourront s'exécuter aussi bien sur un site Web, avec des pages générées généralement côté serveur, que sur un mobile, avec des pages générées localement. Les programmes sont entièrement écrits en OCaml, avec des annotations permettant de décider où les calculs doivent être effectués. Les portions de code client sont compilées vers JavaScript pour être exécutées par une Webview ou un navigateur.

  bio :  Ancien élève de l'École Normale Supérieure de Cachan, Vincent Balat a été maître de conférences à l'université Paris Diderot, puis en délégation chez Inria. Il est le créateur et chef du projet Ocsigen. Il est co-fondateur de BeSport SAS, une entreprise développant un réseau social sur la thématique du sport.  
  
  

• 15:45 - Pause
• 16:15 - LCHIP: architecture double cœur SIL4 pour automatismes sécuritaires à bas coût

  Thierry Lecomte, Clearsy

  L'architecture double cœur SIL4 propose une combinaison astucieuse de principes de sécurisation originaux et s'appuie sur une chaine de développement logicielle formelle éprouvée. Les logiciels, à algorithmique bornée, sont générés et prouvés de manière entièrement automatique, grâce à des outils état de l'art. Les logiciels sont obtenus à partir de DSLs métier orientés ferroviaire et automatismes. Cette architecture, en cours de déploiement pour des applications sécuritaires au Brésil et en Suède, va être améliorée au travers du projet collaboratif LCHIP.

   bio : Thierry Lecomte, directeur  R&D, est en  charge des travaux exploratoires concernant les outils de preuve, les générateurs de code et les outils d'ingénierie pour le développement et la certification de produits ferroviaires et smartcard. 

• 16:45 - Analyse statique sémantique pour la fiabilité des logiciels

  Antoine Miné, LIP6 - Université Pierre et Marie Curie

  Les analyseurs statiques sémantiques infèrent, à la compilation, des propriétés du comportement dynamique des programmes, et donc peuvent éliminer très tôt des classes importantes d'erreurs. L'interprétation abstraite permet la conception de telles analyses, par abstraction calculable de la sémantique des programmes. Elle garantit formellement la sûreté des analyses (éliminant le problème des faux négatifs) et offre des outils pour adapter l'expressivité, la précision et l'efficacité des analyses (limitant le problème des faux positifs). Les méthodes d'analyse basées sur l'interprétation abstraite ont bénéficié, ces dernières années, d'un gain de popularité, notamment par leurs applications à la certification de logiciels embarqués critiques. Dans cet exposé, nous décrirons les caractéristiques principales des analyses statiques de fiabilité logicielle par interprétation abstraite, nous présenterons quelques applications récentes, et nous proposerons quelques pistes afin d'ouvrir leur champ d'application aux logiciels libres.

• 17:15 - Scalable static analysis for security with Abstract interpretation

  Francesco Logozzo, Facebook

  I will introduce Zoncolan, the abstract interpretation-based static analyzer for Hack Facebook's typed PHP) that we built in the last year. Zoncolan focuses on security properties, it is scalable (analyzes millions of lines of code in few minutes), and precise (it is used daily by Facebook security engineers).

   bio : Francesco Logozzo is a software engineer at Facebook. Before he was a researcher for 8 years at Microsoft Research, Redmond, where he co-developed CodeContracts and Clousot, probably the most widely used static analyzer out there. He has strong ties with Paris, he was a postdoc at the ENS Ulm and he did his PhD on abstract interpretation of object oriented languages with Dr. Radhia Cousot at the Ecole Polytechnque.

• 17:45 - Conclusion
• 18:00 - Buffet-networking

 

Inscription gratuite mais obligatoire

Autres journées à venir :

L'Agenda du Libre | Open Source pour le Cloud et les Conteneurs L'Agenda du Libre | Frama-C Day - Analyse et vérification de code L'Agenda du Libre | Techniques de programmation web à l'état de l'art