The Open Source
Innovation Spring 2016

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

Mai-juin 2017, Paris - Villetaneuse - La Défense - Saclay

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 Initiative de Recherche et Innovation sur le Logiciel Libre

Retour à l'OSIS

Frama-C & SPARK Day - Formal Analysis and Proof for Programs in C and Ada

30 Mai 2017 — Frama-C & SPARK Day - Formal Analysis and Proof for Programs in C and Ada


Amphithéâtre Buffon, Paris "Qualité logicielle"


This one-day workshop aims at gathering both academic and industrial users of the environments Frama-C and SPARK, for sharing experiences and discussing perspectives.

It is co-organized by CEA List (, AdaCore (, Inria joint lab `ProofInUse' (, and Université Paris-Diderot.

This workshop will take place in the context of the event `Open Source Innovation Spring 2017' ( initiated by thematic group `Logiciel libre' of the cluster Systematic-Paris-Region and IRILL (`Initiative de Recherche et Innovation sur le Logiciel Libre').

Direction de programme

Programme dirigé par Yannick Moy, AdaCore ; Claude Marché, Inria Saclay ; Florent Kirchner et Nikolai Kosmatov, LIST CEA Tech ; et Mihaela Sighireanu, Université Paris-Diderot.

Description détaillée

Featuring :

  • talks by the Frama-C and SPARK community
  • talks on current developments by the Frama-C and SPARK teams
  • the flair from a central Parisian location

Programme résumé


Amphithéâtre Buffon

Ville: Paris

Organisateurs et/ou sponsors

  • AdaCore

    AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. One of its flagship products is the SPARK Pro verification environment, a toolset based on formal methods and oriented toward high-assurance system.

  • Frama-C

    Frama-C is an extensible and collaborative platform dedicated to source-code analysis of C software.

  • ProofInUse

    ProofInUse originates from the sharing of resources and knowledge between the Toccata research team from Inria and AdaCore, with the objective to provide verification tools, based on mathematical proof, to industry users. These tools are aimed at replacing or complementing the existing test activities, whilst reducing costs.

Organisateurs (2016)

Co-organisateurs et sponsors (2016)

Ils parlent de l'OSIS (2016)

Soutiens du Pôle Systematic