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.

Attachments

Attachments

Posted in #Language    #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.