The SPADE Static Analysis Toolset

The SPADE static analysis suite is the oldest of Praxis High Integrity System's products but one that continues to be used on critical software systems written in languages other than Ada/SPARK.

The SPADE tools provide flow analysis and verification facilities based on a model of the program being analysed. The model is generated by automatic translators which operate on the original source code.

Translators are available for a Pascal subset and for the following assemblers: 68020, 8096 and Z8002.

The SPADE Proof Tools

The SPADE proof tools consist of the Automatic Simplifier and the Proof Checker.

The SPADE Automatic Simplifier discharges many of the more trivial verification conditions generated by SPADE or the SPARK Examiner, simplifying the remainder to make them easier to understand and reason about. For verification conditions to prove the absence of run-time exceptions generated by the SPARK Examiner, the Simplifier's success rate is typically in excess of 75%, reaching over 90% for well-written code which makes good use of types, subtypes and appropriate defensive programming measures.

The SPADE Proof Checker is typically used to discharge the verification conditions which remain to be proved after the Simplifier has been applied. It is a "short-rein" proof assistant, which polices the construction of a valid proof, employing a number of built-in tools and techniques to do so. These include:

• an inference engine, with built-in heuristics for common automatic strategies (for instance, infer A >= C from A >= B and B >= C [transitivity], infer X + N >= Y from X >= Y, N >= 0 [addition of inequalities], etc.);
• a library of several hundred standard proof rules, encapsulating properties of the standard data types appearing in formulae generated for proof of code (such as integers, booleans and enumerated types, arrays, records);
• a range of natural deduction strategies, such as proof by cases, proof by contradiction, proof by induction and subgoaling;
• powerful rule-search and pattern matching facilities, making it easy to select and investigate subexpressions of complex formulae; and
• automatic generation of proof and command logs, allowing the review and replay of proofs, and recording the rules and reasoning employed in the proof of each verification condition.

Releases of the SPADE proof tools have been in industrial use since 1987 and have been employed in the formal verification of a range of high-integrity software systems since that time.

For more information please email us.