SPARK is a high-integrity subset of the Ada programming language. The SPARK Examiner checks conformance of code against the rules of SPARK, performs flow analysis and can generate Verification-Conditions for full formal proof of SPARK source code. In conjunction with the SPADE Simplifier and the SPADE Proof Checker, we can provide a suite of tools capable of aiding the development, testing and verification of safety critical systems written in SPARK Ada.
Spark directory