SPARK Comparison Chart
A look at the expanded features of SPARK included in the SPARK Pro and the SPARK Pro Black Belt Edition.
| Features | SPARK pre-9.0 | SPARK Pro | SPARK Pro Black Belt Edition |
| SPARK toolset (Examiner, Simplifier, and supporting tools) | √ | √ | √ |
| Email support (direct support from product developers) | √ | √ | √ |
| Toolset updates to fix critical bugs | √ | √ | √ |
| Annual releases containing new features and updates | √ | √ | |
| GPS and GNATBench IDEs with support for SPARK | √ | √ | |
| Licensing scheme | FLEXlm | GPL | GPL |
| Subscription scheme based on | Floating Licenses | Total number of engineers | Total number of engineers |
| Access to source code | √ | √ | |
| Availability on Windows and Solaris | √ | √ | √ |
| Availability on Linux and Mac OS X | √ | √ | |
| Access to new enhancements | √ | √ | |
| ZombieScope (detection of dead paths) | √ | √ | |
| Security/safety policy checking | √ | √ | |
| SPARK standard libraries | √ | √ | |
| SPARK Checker (proof assistant) | √ | √ | |
| RavenSPARK language option | √ | √ |