The Open Source
Innovation Spring 2019

Qualité logicielle | IoT | Cloud | Big Data | Systèmes d'information

Mars-juin 2019, Paris - Châtillon

Présidence : Roberto Di Cosmo, vice-président du GTLL, directeur de l’Irill, directeur de recherche Inria, Professeur à l’Université Paris-Diderot

Organisé par : logo Systematic & logo IRILL

Retour à l'OSIS

Langages et Outils pour la Fiabilité Logicielle

12 Mai 2016 — Langages et Outils pour la Fiabilité Logicielle

14h-19h

Jussieu - IRILL, Paris "Qualité logicielle"

Résumé

Augmenter la fiabilité d'un logiciel permet à la fois de diminuer les risques pour ses utilisateurs, et de diminuer ses coûts pour ses concepteurs. Les langages modernes et les outils d'analyse permettent d'aider le développeur considérablement dans cette tâche souvent ingrate.
L'objectif de cette demi-journée, à travers six exposés, est de présenter des approches très diverses, venant aussi bien du monde académique (Lip6-Upmc) que du monde industriel (Facebook) ou des startups (Be Sport) et s'appliquant à des domaines comme l'embarqué critique, avionique (AdaCore) ou ferroviaire (Clearsy) ou la programmation web (Mozilla).

Direction de programme

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

Programme résumé

  • 13:45: Accueil café
  • 14:00: Rust: Systems Programming for Everyone

    Léo Testard, Mozilla

  • 14:00: Introduction

    Emmanuel Chailloux, Roberto Di Cosmo

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

    Raphaël Amiard, Adacore

  • 15:15: Ocsigen: Développement d'applications Web et mobiles client-serveur

    Vincent Balat, BeSport et Univ Paris Diderot

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

    Thierry Lecomte, Clearsy

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

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

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

    Francesco Logozzo, Facebook

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

Lieu

Jussieu - IRILL

Ville: Paris


Programme détaillé

  • 13:45 - Accueil café
  • 14:00 - 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.

  • 14:00 - Introduction

    Emmanuel Chailloux, Roberto Di Cosmo

  • 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. 

  • 15:15 - Ocsigen: Développement d'applications Web et mobiles client-serveur

    Vincent Balat, BeSport et Univ Paris Diderot

    Le Web a subi en quelques années une évolution radicale, passant d'une plateforme de données à une plateforme d'applications. Mais la plupart des outils de programmation n'ont pas été conçus pour cette nouvelle vision du Web. Le projet Ocsigen a pour but d'inventer de nouvelles techniques de programmation adaptées aux besoins des sites Web  modernes et des applications Web distribuées. Il permet de programmer les parties client et serveur dans le même langage, et même, comme une seule et même application. La puissance expressive du langage OCaml permet d'introduire une abstraction des technologies sous-jacentes dans le but de simplifier la programmation d'interactions Web complexes. Le système de types très avancé du langage permet d'améliorer la fiabilité des programmes et le respect des standards.
    Cela permet aussi de réduire beaucoup le temps de développement. Cet exposé donnera un aperçu global du projet et montrera comment BeSport utilise Ocsigen pour développer ses applications Web et mobiles.

    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.

    bio : Professeur à l'Université Pierre et Marie Curie (Paris 6), enseignant au sein de la Faculté d'ingéniérie (UFR 919) et chercheur au Laboratoire d'informatique de Paris 6 (LIP6, UMR 7606) (équipe APR ), Antoine Miné est titulaire d'une thèse en informatique de l'École Polytechnique et d'une habilitation à diriger des recherches de l'École normale supérieure.

  • 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