Formal verification toolset aids certification of safety-critical and high-security systems

January 27, 2016 // By Graham Prophet
The latest release of AdaCore’s SPARK Pro integrated development and verification environment advances the application of mathematics-based static analysis technology to the challenges of software verification for high-assurance systems.

SPARK Pro 16 provides enhanced coverage of SPARK 2014 language features and now supports the Ravenscar tasking profile, thus extending the benefits of formal verification methods to a safe subset of Ada 2012 concurrent programming features. As another improvement SPARK Pro 16 can generate counterexamples to verification conditions that cannot be proved, thus making it easier for developers to find defects in the functional code or in the supplied contracts. SPARK Pro 16 also improves the handling of bitwise (modular) operations, and the product’s proof engine now includes the Z3 SMT solver.

The SPARK Pro technology, which has been jointly developed by AdaCore and its partner Altran, can prove SPARK program properties ranging from absence of run-time errors (exceptions) to compliance with a formally defined requirements specification. SPARK Pro thereby helps reduce the cost of software verification and simplifies the task of certifying the software against safety or security standards. The technology is sound; that is, there are no “false negatives”: if SPARK Pro reports that a program is free of a certain kind of error, then that error cannot occur. It also has a very low “false positive” rate, which is important in practice, and its efficient SMT solver technology scales up for usage in large projects. The SPARK language and toolset can be used from the outset on new projects or introduced incrementally into an existing project, allowing a “hybrid” verification approach that combines formal methods with traditional testing techniques.

“With this new version of the SPARK Pro toolset, we get one step closer to our goal: to make it easy for software engineers to start relying heavily on static verification and formal proofs without needing expertise in mathematical logic,” said Cyrille Comar, AdaCore President. “Not only are most of the needed proofs conducted completely automatically, but many language restrictions usually associated with such proof capabilities have been lifted. This makes the writing of proven software both