Yannick Moy, AdaCore
Five years after the official adoption of the new DO-178C/ED-12C standard and its supplements, including the DO-333/ED-216 supplement on formal methods, no avionics-certification project has yet acknowledged using this new supplement. However, formal method technologies do exist that would ease the development of avionics software.
While Ada offers many features that act as safety guards at run time, by raising exceptions when a violation is detected, some of these features may be too complex to guarantee a safe execution before the program is run. This is the case for example of pointers, which may be used to create arbitrarily complex shared data structures in memory. SPARK is a subset of Ada that forbids these features, most notably pointers, in order to be able to provide strong guarantees at compile time. A preview of the next revision of SPARK called SPARK 2014 is already available, as well as the associated verification tools.