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 m...
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.