The paper attached titled "A Proof Infrastructure for Binary Programs" is the result of two years of work by researchers from Dependable Computing and Zephyr Software LLC. This is an interesting use of SPARK as an intermediate language. Other uses of SPARK as intermediate language are from code generation for modeling languages such as Simulink (in QGen qualifiable code generator) and SCADE (in KCG qualified code generator). It's interesting to see the reasons for which these researchers chose SPARK as intermediate language in this work (quoted from the article):

• The SPARK Ada language has been designed for proof and includes syntactic structures to enable definition of the necessary verification conditions.
• SPARK Ada is familiar to many in the community and simple to use.
• SPARK Pro proof tools provide the capability to establish necessary proofs.
• SPARK Pro has industrial-strength support thereby allowing the technology to be adopted by practitioners.
• SPARK Pro provides an executable specification that can be tested.

These are indeed the main goals we have pursued with SPARK, so we're glad to see these researchers agreeing with us on these points. We also happen to agree with their conclusion:

"The SPARKPro toolchain has the advantage of being able to run multiple proofs in parallel with most proofs discharged automatically. Additionally, the SPARK Ada representation can be compiled into an executable program that could allow for verification by testing for representational accuracy. A current disadvantage of the toolchain is that, when proofs are not discharged automatically, completing the proof manually can be difficult."

Providing a smoother path from fully automatic proof to inclusion of manual proof is one of the main goals we're pursuing now, with recent advances being made in a new SPARK lemma library. For the current features in SPARK for manual proof, see examples in the SPARK User's Guide.

Legal notice: the original source for the attached article is copyrighted and published by Springer, published here by special authorization of Springer.