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.
Co-Developing Programs and Their Proof of Correctness
Explore SPARK's future in high-integrity systems with the ACM paper on co-developing programs and their correctness proofs. Download the Technical Paper.
Download 1.8 MB pdf