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.
This workshop will take place in the context of the event `Open Source Innovation Spring 2017' (http://www.open-source-innovation-spring.org/) initiated by thematic group `Logiciel libre' of the cluster Systematic-Paris-Region and IRILL (`Initiative de Recherche et Innovation sur le Logiciel Libre').
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 is an extensible and collaborative platform dedicated to source-code analysis of C software.
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.