SPARK is a software development technology (programming language and verification toolset) specifically designed for engineering ultra-low-defect-level applications, for example where safety and/or security are key requirements. SPARK Pro is the commercial-grade offering of the SPARK technology developed by AdaCore, Altran and Inria.
SPARK has an extensive industrial track record. Since its inception in the late 1980s it has been used worldwide in a range of industrial applications such as civil and military avionics, air traffic management/control, railway signaling, cryptographic software, cross-domain solutions, medical devices and automotive.
The SPARK language is a large subset of Ada 2012. SPARK includes as much of Ada as is possible/practical to analyze formally, while eliminating sources of undefined and implementation- dependent behavior. SPARK includes Ada’s program-structure support (packages, generics, child libraries), most data types, safe pointers, contract-based programming (subprogram pre- and postconditions, scalar ranges, type/subtype predicates), Object-Oriented Programming, and the Ravenscar subset of tasking features.
