Co-Developing Programs and Their Proof of Correctness

We’re excited 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, including: an overview of the programming language and its design goals; an explanation of what it means to co-develop a program and its proof of correctness; and approaches to practical, incremental adoption that allow at-scale application to industrial, high-integrity systems.