AdaCore Blog

Use of SPARK in a Certification Context

by Yannick Moy

One possible reason to choose SPARK over other solutions is the benefits that it brings in a certification context, for reaching some of the verification objectives. For example, the previous version of SPARK has been used both in a safety certification context and in a security certification context. With SPARK 2014, we target in particular the avionics domain, whose recently updated certification standard DO-178C accepts the use of formal verification as justification for many verification objectives.

While certification authorities in railway have long recognized the use of formal methods, and a few companies like Airbus and Rockwell Collins have pioneered the use of formal methods in avionics, we still are at the beginning of the adoption of formal methods in industries submitted to certification constraints. Which means that many people simply don't know yet how they should present the use of formal methods to the certification authorities to obtain the credit they expect from it.

This was the reason that pushed in 2010 for the creation of the workshop on Theorem Proving in Certification. Since then, the group has had 3 gatherings in Oxford, the last of which in December last year, during which we decided to work on a shared document gathering recommandations for the use of formal methods in certification. This draft document is now publicly available here:

If you're interested in this topic, don't hesitate to send comments about the above document to the public mailing-list You can also participate more actively in the discussions by joining the googlegroup.

Posted in #Formal Verification    #Certification   

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 Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.