- Introduction
This repository contains the source code for the SPARK 2014 project. SPARK is a software development technology specifically designed for engineering high-reliability applications. It consists of a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements.
- Commercial support
SPARK is commercially supported by AdaCore and Altran, you can visit the AdaCore website for more information.
- GPL version
There is a GPL version of the tools, readily packaged, and suitable for research and hobbyist use. You can download it from [libre.adacore.com] (http://libre.adacore.com/download/).
- Community
News about SPARK project are shared primarily on a dedicated blog. Discussions about SPARK occur on a public mailing-list.
- Documentation
You can find the definition of the SPARK language in the SPARK Reference Manual, and instructions on how to use the tool, together with a tutorial, in the SPARK User's Guide.