I am delighted to announce that the Communications of the ACM has published a paper on SPARK: “Co-Developing Programs and Their Proof of Correctness”. The paper provides a comprehensive and up-to-date presentation of SPARK; as such, it’s a great reference to share with anyone - in industry, academia, or anywhere in between - who might like to know more about SPARK.

In the paper, you’ll find:

• A thorough presentation of the latest version of the SPARK language. The paper describes the design rationale behind the SPARK language, including the tradeoffs that must be made to permit sound analysis. It presents some of the most recent features that have been added, including support for pointers via an ownership model.
  
  

• An explanation of what it means to co-develop a program and its proof of correctness through the auto-active approach: by introducing “ghost code” users not only specify the behavior of their software, they can also guide the proof engines to proofs of correctness, when required. The paper presents examples of typical proof patterns that require the auto-active approach.

• A practical discussion of how SPARK can be adopted. The paper describes different levels of SPARK adoption, starting with adapting some part of a program to the SPARK subset, continuing on to flow analysis, stepping up to proof of absence of runtime exceptions, and ultimately achieving proof of functional correctness. The key observation is that SPARK brings value at each level of adoption, even if the entirety of the program is not written in SPARK.

Be sure you don’t miss the paper’s two sidebars:

• A brief recap of Rod’s work on SPARKNaCl

• A brief recap of NVIDIA’s use of SPARK

Congratulations to Rod, Claire, Stuart, and Yannick!