AdaCore Blog

Rail, Space, Security: Three Case Studies for SPARK 2014

by Yannick Moy

Since 2010, while we developed the language and toolset for SPARK 2014, David Lesens from Astrium Space Transportation has developed an extensive case study in the space domain using the prototypes we produced. On a smaller scale, David Mentré from Mitsubishi Electric R&D Centre Europe has developed a case study in the rail domain, and more recently Pavlos Efstathopoulos from Altran UK Limited has developed a case study in the security domain. The results of these three case studies are presented in the paper we will publish at ERTS 2014.



Posted in #Language    #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy

Yannick Moy is Static Analysis Lead at AdaCore and co-director of the ProofInUse joint laboratory with Inria. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.